src/HOL/Prod.ML
changeset 1160 8845eb5f0e5e
parent 972 e61b058d58d2
child 1264 3eb91524b938