src/HOL/Prod.ML
changeset 6392 e2ecfd8622ae
parent 6016 797c76d6ff04
child 6394 3d9fd50fcc43