src/HOL/Prod.ML
changeset 2250 891eb76b8045
parent 2089 e2ec077ac90d
child 2637 e9b203f854ae