src/HOL/FunDef.thy
changeset 54492 6fae4ecd4ab3
parent 54407 e95831757903