changeset 15600 | a59f07556a8d |
parent 15593 | 24d770bbc44a |
child 15609 | d12c459e2325 |
15599:10cedbd5289e | 15600:a59f07556a8d |
---|---|
1 (* Title: HOLCF/Cprod1.thy |
1 (* Title: HOLCF/Cprod.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 Partial ordering for cartesian product of HOL theory prod.thy |
6 Partial ordering for cartesian product of HOL theory prod.thy |