HomeIsabelle/Phabricator

avoid [no_atp] declations shadowing propositions from sledgehammer