src/HOL/Fun_Def.thy
changeset 64448 49b78f1f9e01
parent 63654 f90e3926e627
child 64591 240a39af9ec4
equal deleted inserted replaced
64447:e44f5c123f26 64448:49b78f1f9e01