src/HOL/Prod.thy
changeset 4707 abe6f28a38c1
parent 4570 c04027ccc86e
child 4875 cb48549230ce