src/HOL/Prod.thy
changeset 9634 61b57cc1cb5a
parent 9360 82e8b18e6985