HomeIsabelle/Phabricator

removed redundant T_xxx_bound_aux lemmas