src/HOL/Prod.ML
changeset 6738 06189132c67b
parent 6394 3d9fd50fcc43
child 6830 f8aed3706af7