src/HOL/Prod.thy
changeset 3718 d78cf498a88c
parent 3692 9f9bcce140ce
child 3842 b55686a7b22c