src/HOL/Prod.thy
changeset 3044 3e3087aa69e7
parent 2973 184c7cd8043d
child 3692 9f9bcce140ce