src/HOL/Fun_Def.thy
changeset 64715 33d5fa0ce6e5
parent 64591 240a39af9ec4
child 67443 3abf6a722518
equal deleted inserted replaced
64714:53bab28983f1 64715:33d5fa0ce6e5