HomeIsabelle/Phabricator

extraction of equations x = t from premises beneath meta-all