--- a/src/HOLCF/ssum3.thy Sat Apr 05 17:03:38 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(* Title: HOLCF/ssum3.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Class instance of ++ for class pcpo
-*)
-
-Ssum3 = Ssum2 +
-
-arities "++" :: (pcpo,pcpo)pcpo (* Witness ssum2.ML *)
-
-consts
- sinl :: "'a -> ('a++'b)"
- sinr :: "'b -> ('a++'b)"
- when :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
-
-rules
-
-inst_ssum_pcpo "UU::'a++'b = Isinl(UU)"
-
-sinl_def "sinl == (LAM x.Isinl(x))"
-sinr_def "sinr == (LAM x.Isinr(x))"
-when_def "when == (LAM f g s.Iwhen(f)(g)(s))"
-
-end
-
-
-