src/HOL/ex/Recdefs.ML
changeset 6099 d4866f6ff2f9
parent 5655 afd75136b236
child 6451 bc943acc5fda