src/HOL/FunDef.thy
changeset 20618 3f763be47c2f
parent 20536 f088edff8af8
child 20654 d80502f0d701