src/HOL/Prod.ML
changeset 3718 d78cf498a88c
parent 3568 36ff1ab12021
child 3842 b55686a7b22c