src/HOL/Fun_Def.thy
changeset 80743 94e64d8ac668
parent 80322 b10f7c981df6