src/HOL/FunDef.thy
changeset 54574 d04e74341d43
parent 54407 e95831757903