src/HOL/ex/Recdefs.ML
changeset 5694 39af7b3dd1c4
parent 5655 afd75136b236
child 6451 bc943acc5fda
equal deleted inserted replaced
5693:998af7667fa3 5694:39af7b3dd1c4