IMP/Denotation.thy

--- a/IMP/Denotation.thy	Fri Apr 14 11:23:33 1995 +0200
+++ b/IMP/Denotation.thy	Wed Jun 21 15:12:40 1995 +0200
@@ -30,17 +30,17 @@
   B_or	  "B(b0 ori b1) = (%s. B(b0,s) | B(b1,s))"
 
 defs
-  Gamma_def	"Gamma(b,cd) ==   \
-\		   (%phi.{st. st : (phi O cd) & B(b,fst(st))} Un \
-\	                 {st. st : id & ~B(b,fst(st))})"
+  Gamma_def	"Gamma(b,cd) ==   
+		   (%phi.{st. st : (phi O cd) & B(b,fst(st))} Un 
+	                 {st. st : id & ~B(b,fst(st))})"
 
 primrec C com
   C_skip    "C(skip) = id"
   C_assign  "C(x := a) = {st . snd(st) = fst(st)[A(a,fst(st))/x]}"
   C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
-  C_if	    "C(ifc b then c0 else c1) =   \
-\		   {st. st:C(c0) & B(b,fst(st))} Un \
-\	           {st. st:C(c1) & ~B(b,fst(st))}"
+  C_if	    "C(ifc b then c0 else c1) =   
+		   {st. st:C(c0) & B(b,fst(st))} Un 
+	           {st. st:C(c1) & ~B(b,fst(st))}"
   C_while   "C(while b do c) = lfp(Gamma(b,C(c)))"
 
 end