src/HOL/FunDef.thy
changeset 24000 467e77e4e276
parent 23739 c5ead5df7f35
child 24162 8dfd5dd65d82