src/HOL/Prod.thy
changeset 3362 0b268cff9344
parent 2973 184c7cd8043d
child 3692 9f9bcce140ce