| changeset 13897 | f62f9a75f685 |
| parent 13896 | 717bd79b976f |
| child 13898 | 9410d2eb9563 |
| 13896:717bd79b976f | 13897:f62f9a75f685 |
|---|---|
1 (* Title: HOLCF/sprod2.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Class Instance **::(pcpo,pcpo)po |
|
7 *) |
|
8 |
|
9 Sprod2 = Sprod1 + |
|
10 |
|
11 arities "**" :: (pcpo,pcpo)po |
|
12 |
|
13 (* Witness for the above arity axiom is sprod1.ML *) |
|
14 |
|
15 rules |
|
16 |
|
17 (* instance of << for type ['a ** 'b] *) |
|
18 |
|
19 inst_sprod_po "(op <<)::['a ** 'b,'a ** 'b]=>bool = less_sprod" |
|
20 |
|
21 end |
|
22 |
|
23 |
|
24 |