src/HOL/FunDef.thy
changeset 36288 156e4f179bb0
parent 34228 bc0cea4cae52
child 36521 73ed9f18fdd3
equal deleted inserted replaced
36287:96f45c5ffb36 36288:156e4f179bb0