src/HOL/Fun_Def.thy
changeset 66759 918f15c9367a
parent 64591 240a39af9ec4
child 67443 3abf6a722518
equal deleted inserted replaced
66758:9312ce5a938d 66759:918f15c9367a