src/HOL/FunDef.thy
changeset 47019 7bdac8e81f6d
parent 46950 d0181abdbdac
child 47432 e1576d13e933