diff -r 85ecd3439e01 -r 03f096efa26d src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Tue Feb 06 12:44:31 1996 +0100
+++ b/src/HOL/IMP/Denotation.thy	Wed Feb 07 12:22:32 1996 +0100
@@ -35,12 +35,12 @@
                          {st. st : id & ~B b (fst st)})"
 
 primrec C com
-  C_skip    "C(skip) = id"
+  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) =   
+  C_if      "C(IF 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))"
+  C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
 
 end