diff -r c3913a79b6ae -r 492493334e0f 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