| changeset 13897 | f62f9a75f685 |
| parent 13896 | 717bd79b976f |
| child 13898 | 9410d2eb9563 |
| 13896:717bd79b976f | 13897:f62f9a75f685 |
|---|---|
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 |