HomeIsabelle/Phabricator

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