changeset 243 | c22b85994e17 |
child 442 | 13ac1fd0a14d |
242:8fe3e66abf0c | 243:c22b85994e17 |
---|---|
1 (* Title: HOLCF/ssum2.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Class Instance ++::(pcpo,pcpo)po |
|
7 *) |
|
8 |
|
9 Ssum2 = Ssum1 + |
|
10 |
|
11 arities "++" :: (pcpo,pcpo)po |
|
12 (* Witness for the above arity axiom is ssum1.ML *) |
|
13 |
|
14 rules |
|
15 |
|
16 (* instance of << for type ['a ++ 'b] *) |
|
17 |
|
18 inst_ssum_po "(op <<)::['a ++ 'b,'a ++ 'b]=>bool = less_ssum" |
|
19 |
|
20 end |
|
21 |
|
22 |
|
23 |