src/HOL/Prod.ML
changeset 2279 2f337bf81085
parent 2089 e2ec077ac90d
child 2637 e9b203f854ae