src/HOL/FunDef.thy
changeset 40602 91e583511113
parent 40108 dbab949c2717
child 46526 c4cf9d03c352
equal deleted inserted replaced
40598:16742772a9b3 40602:91e583511113