src/HOL/Prod.ML
changeset 1444 23ceb1dc9755
parent 1301 42782316d510
child 1454 d0266c81a85e