# HG changeset patch
# User wenzelm
# Date 1368781559 -7200
# Node ID 0476162187c484920f4dc2adca01efc12016689e
# Parent  bc01725d79182d7940057dd5863d6ce66d6bb268
repair after bc01725d7918;

diff -r bc01725d7918 -r 0476162187c4 src/HOL/HOLCF/IMP/Denotational.thy
--- a/src/HOL/HOLCF/IMP/Denotational.thy	Fri May 17 08:19:52 2013 +0200
+++ b/src/HOL/HOLCF/IMP/Denotational.thy	Fri May 17 11:05:59 2013 +0200
@@ -17,7 +17,7 @@
 where
   "D(SKIP) = (LAM s. Def(undiscr s))"
 | "D(X ::= a) = (LAM s. Def((undiscr s)(X := aval a (undiscr s))))"
-| "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
+| "D(c0 ;; c1) = (dlift(D c1) oo (D c0))"
 | "D(IF b THEN c1 ELSE c2) =
         (LAM s. if bval b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)"
 | "D(WHILE b DO c) =