| changeset 243 | c22b85994e17 |
| child 1150 | 66512c9e6bd6 |
| 242:8fe3e66abf0c | 243:c22b85994e17 |
|---|---|
1 (* Title: HOLCF/cprod1.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 |
|
7 Partial ordering for cartesian product of HOL theory prod.thy |
|
8 |
|
9 *) |
|
10 |
|
11 Cprod1 = Cfun3 + |
|
12 |
|
13 |
|
14 consts |
|
15 less_cprod :: "[('a::pcpo * 'b::pcpo),('a * 'b)] => bool" |
|
16 |
|
17 rules |
|
18 |
|
19 less_cprod_def "less_cprod(p1,p2) == ( fst(p1) << fst(p2) &\ |
|
20 \ snd(p1) << snd(p2))" |
|
21 |
|
22 end |
|
23 |