src/HOL/FunDef.thy
changeset 36070 d80e5d3c8fe1
parent 34228 bc0cea4cae52
child 36521 73ed9f18fdd3
equal deleted inserted replaced
36057:ca6610908ae9 36070:d80e5d3c8fe1