src/HOL/IMP/Denotation.thy

--- a/src/HOL/IMP/Denotation.thy	Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/IMP/Denotation.thy	Fri Oct 02 14:28:39 1998 +0200
@@ -19,7 +19,7 @@
   C     :: com => com_den
 
 primrec
-  C_skip    "C(SKIP) = id"
+  C_skip    "C(SKIP) = Id"
   C_assign  "C(x := a) = {(s,t). t = s[x:=a(s)]}"
   C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
   C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
@@ -27,5 +27,3 @@
   C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
 
 end
-
-