src/HOL/FunDef.thy
changeset 22320 d5260836d662
parent 22268 ee2619267dca
child 22324 c95319d14332