src/HOL/FunDef.thy
changeset 47259 2d4ea84278da
parent 46950 d0181abdbdac
child 47432 e1576d13e933