src/HOL/Fun_Def.thy
changeset 65677 7d25b8dbdbfa
parent 64591 240a39af9ec4
child 67443 3abf6a722518
equal deleted inserted replaced
65676:c9c352583b16 65677:7d25b8dbdbfa