src/HOL/FunDef.thy
changeset 39733 6d373e9dcb9d
parent 37767 a2b7a20d6ea3
child 40108 dbab949c2717
equal deleted inserted replaced
39732:4dbc72759706 39733:6d373e9dcb9d