src/HOL/Prod.thy
changeset 9955 6ed42bcba707
parent 9360 82e8b18e6985