src/HOL/ex/Fundefs.thy
changeset 25517 36d710d1dbce
parent 25170 bd06fd396fd0
child 25680 909bfa21acc2