src/HOL/Fun_Def_Base.thy
changeset 55370 e6be866b5f5b
parent 55085 0e8e4dc55866
child 55968 94242fa87638
equal deleted inserted replaced
55369:713629c2b73c 55370:e6be866b5f5b