changeset 243 | c22b85994e17 |
child 442 | 13ac1fd0a14d |
242:8fe3e66abf0c | 243:c22b85994e17 |
---|---|
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 |