src/HOL/FunDef.thy
changeset 26583 9f81ab1b7b64
parent 25567 5720345ea689
child 26748 4d51ddd6aa5c