equal
deleted
inserted
replaced
1 (* Title: HOLCF/sprod1.thy |
1 (* Title: HOLCF/sprod1.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 Copyright 1993 Technische Universitaet Muenchen |
4 Copyright 1993 Technische Universitaet Muenchen |
5 |
5 |
6 Partial ordering for the strict product |
6 Partial ordering for the strict product |
7 *) |
7 *) |
8 |
8 |
9 Sprod1 = Sprod0 + |
9 Sprod1 = Sprod0 + |
10 |
10 |
11 consts |
11 consts |
12 less_sprod :: "[('a ** 'b),('a ** 'b)] => bool" |
12 less_sprod :: "[('a ** 'b),('a ** 'b)] => bool" |
13 |
13 |
14 defs |
14 defs |
15 less_sprod_def "less_sprod p1 p2 == |
15 less_sprod_def "less_sprod p1 p2 == |
16 if p1 = Ispair UU UU |
16 if p1 = Ispair UU UU |
17 then True |
17 then True |
18 else Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2" |
18 else Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2" |
19 |
19 |
20 end |
20 end |