src/HOL/Prod.ML
changeset 1201 de2fc8cf9b6a
parent 972 e61b058d58d2
child 1264 3eb91524b938
equal deleted inserted replaced
1200:d4551b1a6da7 1201:de2fc8cf9b6a