src/HOL/FunDef.thy
changeset 47534 06cc372a80ed
parent 47432 e1576d13e933
child 47701 157e6108a342