src/HOL/Fun.thy
changeset 3257 4e3724e0659f
parent 2912 3fac3e8d5d3e
child 4059 59c1422c9da5
equal deleted inserted replaced
3256:0a45cdd7da37 3257:4e3724e0659f