src/HOL/Fun_Def_Base.thy
changeset 60621 bfb14ff43491
parent 58889 5b7a9633cfa8
child 60758 d8d85a8172b5
equal deleted inserted replaced
60620:41e180848d02 60621:bfb14ff43491