src/HOL/Fun_Def.thy
changeset 56978 0c1b4987e6b2
parent 56846 9df717fef2bb
child 57959 1bfed12a7646