src/HOL/Prod.ML
changeset 2638 6c6a44b5f757
parent 2637 e9b203f854ae
child 2856 cdb908486a96
equal deleted inserted replaced
2637:e9b203f854ae 2638:6c6a44b5f757