src/HOL/FunDef.thy
changeset 23315 df3a7e9ebadb
parent 23203 a5026e73cfcf
child 23494 f985f9239e0d