src/HOL/FunDef.thy
changeset 23386 9255c1a75ba9
parent 23203 a5026e73cfcf
child 23494 f985f9239e0d
equal deleted inserted replaced
23385:0ef4f9fc0d09 23386:9255c1a75ba9