src/HOL/FunDef.thy
changeset 47678 c04b223d661e
parent 47432 e1576d13e933
child 47701 157e6108a342