src/HOL/FunDef.thy
changeset 52463 c45a6939217f
parent 49989 34d0ac1bdac6
child 53603 59ef06cda7b9
equal deleted inserted replaced
52462:a241826ed003 52463:c45a6939217f