src/HOL/ex/Recdef.ML
changeset 4834 dd89afb55272
parent 4686 74a12e86b20b
child 5069 3ea049f7979d