src/HOL/Fun_Def.thy
changeset 61766 507b39df1a57
parent 61032 b57df8eecad6
child 61799 4cf66f21b764
equal deleted inserted replaced
61765:13ca8f4f6907 61766:507b39df1a57