src/HOL/Prod.ML
changeset 2651 60d8d06f84a5
parent 2637 e9b203f854ae
child 2856 cdb908486a96