src/HOL/ex/Fundefs.thy
changeset 44335 156be0e43336
parent 41817 c7be23634728
child 45008 8b74cfea913a