src/HOL/Fun_Def.thy
changeset 65371 ce09e947c1d5
parent 64591 240a39af9ec4
child 67443 3abf6a722518
equal deleted inserted replaced
65370:1324268c2f6a 65371:ce09e947c1d5