src/HOL/FunDef.thy
changeset 24052 90dd4df2c7c3
parent 23739 c5ead5df7f35
child 24162 8dfd5dd65d82