src/HOL/FunDef.thy
changeset 48559 686cc7c47589
parent 47701 157e6108a342
child 48891 c0eafbd55de3