--- a/src/HOL/IMP/Denotation.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IMP/Denotation.thy Wed Jun 21 15:47:10 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