src/HOL/FunDef.thy
changeset 47197 ed681ca1188a
parent 46950 d0181abdbdac
child 47432 e1576d13e933