src/HOL/FunDef.thy
changeset 35888 d902054e7ac6
parent 34228 bc0cea4cae52
child 36521 73ed9f18fdd3
equal deleted inserted replaced
35887:f704ba9875f6 35888:d902054e7ac6