src/HOL/FunDef.thy
changeset 47647 ec29cc09599d
parent 47432 e1576d13e933
child 47701 157e6108a342