src/HOL/FunDef.thy
changeset 54924 44373f3560c7
parent 54407 e95831757903