src/HOL/Prod.ML
changeset 3362 0b268cff9344
parent 2935 998cb95fdd43
child 3429 160f18a686b5