src/HOL/Fun.thy
changeset 48610 0095de9e9da0
parent 47579 28f6f4ad69bf
child 48891 c0eafbd55de3
equal deleted inserted replaced
48609:0090fab725e3 48610:0095de9e9da0