src/HOL/Fun_Def_Base.thy
changeset 55147 bce3dbc11f95
parent 55085 0e8e4dc55866
child 55968 94242fa87638