src/HOL/FunDef.thy
changeset 22009 b0c966b30066
parent 21512 3786eb1b69d6
child 22166 0a50d4db234a