src/HOL/FunDef.thy
changeset 54610 6593e06445e6
parent 54407 e95831757903