src/HOL/Prod.ML
changeset 7360 7d3136b9af08
parent 7339 1b4d7a851b34
child 7495 affcfd2830b7