src/HOL/Prod.thy
changeset 1578 b58a6182e184
parent 1558 9c6ebfab4e05
child 1636 e18416e3e1d4