src/HOL/Prod.ML
changeset 5936 406eb27fe53c
parent 5810 829cae93f132
child 6016 797c76d6ff04