src/HOL/FunDef.thy
changeset 23853 2c69bb1374b8
parent 23739 c5ead5df7f35
child 24162 8dfd5dd65d82