src/HOL/ex/Fundefs.thy
changeset 48927 ef462b5558eb
parent 45008 8b74cfea913a
child 53611 437c0a63bb16