src/HOL/FunDef.thy
changeset 21316 4d913b8bccf1
parent 21312 1d39091a3208
child 21319 cf814e36f788