HomeIsabelle/Phabricator

library theory for extractions of equations x = t into premises