src/HOL/FunDef.thy
changeset 25836 f7771e4f7064
parent 25567 5720345ea689
child 26748 4d51ddd6aa5c