src/HOL/FunDef.thy
changeset 19647 043921b0e587
parent 19564 d3e2f532459a
child 19770 be5c23ebe1eb