src/HOL/ex/Fundefs.thy
changeset 25001 7982fe02a50e
parent 24585 c359896d0f48
child 25170 bd06fd396fd0