src/HOL/ex/Recdefs.ML
changeset 9380 63cca60b2cce
parent 8683 9d3e8c4a0287
child 9736 332fab43628f