src/HOL/ex/Recdefs.ML
changeset 6213 f5bdd6497e08
parent 5655 afd75136b236
child 6451 bc943acc5fda