src/HOL/FunDef.thy
changeset 36271 2ef9dbddfcb8
parent 34228 bc0cea4cae52
child 36521 73ed9f18fdd3
equal deleted inserted replaced
36262:d7d1d87276b7 36271:2ef9dbddfcb8