src/HOL/Prod.thy
changeset 4732 10af4886b33f
parent 4570 c04027ccc86e
child 4875 cb48549230ce