src/HOL/Prod.ML
changeset 6260 a8010d459ef7
parent 6016 797c76d6ff04
child 6394 3d9fd50fcc43