src/HOL/FunDef.thy
changeset 26157 4d9d0a26c32a
parent 25567 5720345ea689
child 26748 4d51ddd6aa5c
equal deleted inserted replaced
26156:420c1947511c 26157:4d9d0a26c32a