src/HOL/Prod.ML
changeset 3079 2ea678d3523f
parent 2935 998cb95fdd43
child 3429 160f18a686b5
equal deleted inserted replaced
3078:984866a8f905 3079:2ea678d3523f