src/HOL/Fun_Def.thy
changeset 75670 acf86c9f7698
parent 75669 43f5dfb7fa35
child 79597 76a1c0ea6777
equal deleted inserted replaced
75669:43f5dfb7fa35 75670:acf86c9f7698