src/HOL/FunDef.thy
changeset 21378 cedfce6fc725
parent 21364 3baf57a27269
child 21404 eb85850d3eb7