HomeIsabelle/Phabricator

added simp lemma

Authored by nipkow.