src/HOL/FunDef.thy
changeset 21234 fb84ab52f23b
parent 21211 5370cfbf3070
child 21312 1d39091a3208
equal deleted inserted replaced
21233:5a5c8ea5f66a 21234:fb84ab52f23b