src/HOL/Prod.ML
changeset 7188 2bc63a44721b
parent 7031 972b5f62f476
child 7339 1b4d7a851b34