HomeIsabelle/Phabricator

factored out auxiliary theory