src/HOL/IMP/Denotation.thy
changeset 1151 c820b3cc3df0
parent 924 806721cfbf46
child 1374 5e407f2a3323
     1.1 --- a/src/HOL/IMP/Denotation.thy	Wed Jun 21 15:14:58 1995 +0200
     1.2 +++ b/src/HOL/IMP/Denotation.thy	Wed Jun 21 15:47:10 1995 +0200
     1.3 @@ -30,17 +30,17 @@
     1.4    B_or	  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
     1.5  
     1.6  defs
     1.7 -  Gamma_def	"Gamma b cd ==   \
     1.8 -\		   (%phi.{st. st : (phi O cd) & B b (fst st)} Un \
     1.9 -\	                 {st. st : id & ~B b (fst st)})"
    1.10 +  Gamma_def	"Gamma b cd ==   
    1.11 +		   (%phi.{st. st : (phi O cd) & B b (fst st)} Un 
    1.12 +	                 {st. st : id & ~B b (fst st)})"
    1.13  
    1.14  primrec C com
    1.15    C_skip    "C(skip) = id"
    1.16    C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
    1.17    C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    1.18 -  C_if	    "C(ifc b then c0 else c1) =   \
    1.19 -\		   {st. st:C(c0) & (B b (fst st))} Un \
    1.20 -\	           {st. st:C(c1) & ~(B b (fst st))}"
    1.21 +  C_if	    "C(ifc b then c0 else c1) =   
    1.22 +		   {st. st:C(c0) & (B b (fst st))} Un 
    1.23 +	           {st. st:C(c1) & ~(B b (fst st))}"
    1.24    C_while   "C(while b do c) = lfp (Gamma b (C c))"
    1.25  
    1.26  end