src/HOL/Fun_Def.thy
changeset 57874 9c361f94b323
parent 56846 9df717fef2bb
child 57959 1bfed12a7646