src/HOL/FunDef.thy
changeset 40396 c4c6fa6819aa
parent 40108 dbab949c2717
child 46526 c4cf9d03c352
equal deleted inserted replaced
40395:4985aaade799 40396:c4c6fa6819aa