equal
deleted
inserted
replaced
1 (* Title: HOLCF/ssum3.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Class instance of ++ for class pcpo |
|
7 *) |
|
8 |
|
9 Ssum3 = Ssum2 + |
|
10 |
|
11 arities "++" :: (pcpo,pcpo)pcpo (* Witness ssum2.ML *) |
|
12 |
|
13 consts |
|
14 sinl :: "'a -> ('a++'b)" |
|
15 sinr :: "'b -> ('a++'b)" |
|
16 when :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c" |
|
17 |
|
18 rules |
|
19 |
|
20 inst_ssum_pcpo "UU::'a++'b = Isinl(UU)" |
|
21 |
|
22 sinl_def "sinl == (LAM x.Isinl(x))" |
|
23 sinr_def "sinr == (LAM x.Isinr(x))" |
|
24 when_def "when == (LAM f g s.Iwhen(f)(g)(s))" |
|
25 |
|
26 end |
|
27 |
|
28 |
|
29 |
|