src/HOL/Fun_Def.thy
changeset 81964 8efec8da78f9
parent 80322 b10f7c981df6