src/HOL/IMP/Denotation.thy
changeset 5608 a82a038a3e7a
parent 5183 89f162de39cf
child 9241 f961c1fdff50
     1.1 --- a/src/HOL/IMP/Denotation.thy	Fri Oct 02 10:44:20 1998 +0200
     1.2 +++ b/src/HOL/IMP/Denotation.thy	Fri Oct 02 14:28:39 1998 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    C     :: com => com_den
     1.5  
     1.6  primrec
     1.7 -  C_skip    "C(SKIP) = id"
     1.8 +  C_skip    "C(SKIP) = Id"
     1.9    C_assign  "C(x := a) = {(s,t). t = s[x:=a(s)]}"
    1.10    C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    1.11    C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
    1.12 @@ -27,5 +27,3 @@
    1.13    C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
    1.14  
    1.15  end
    1.16 -
    1.17 -