--- a/src/HOLCF/Ssum1.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Ssum1.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/ssum1.thy
+(* Title: HOLCF/ssum1.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Partial ordering for the strict sum ++
@@ -10,15 +10,15 @@
consts
- less_ssum :: "[('a ++ 'b),('a ++ 'b)] => bool"
+ less_ssum :: "[('a ++ 'b),('a ++ 'b)] => bool"
rules
less_ssum_def "less_ssum s1 s2 == (@z.
- (! u x.s1=Isinl(u) & s2=Isinl(x) --> z = (u << x))
- &(! v y.s1=Isinr(v) & s2=Isinr(y) --> z = (v << y))
- &(! u y.s1=Isinl(u) & s2=Isinr(y) --> z = (u = UU))
- &(! v x.s1=Isinr(v) & s2=Isinl(x) --> z = (v = UU)))"
+ (! u x.s1=Isinl(u) & s2=Isinl(x) --> z = (u << x))
+ &(! v y.s1=Isinr(v) & s2=Isinr(y) --> z = (v << y))
+ &(! u y.s1=Isinl(u) & s2=Isinr(y) --> z = (u = UU))
+ &(! v x.s1=Isinr(v) & s2=Isinl(x) --> z = (v = UU)))"
end