# HG changeset patch
# User nipkow
# Date 1371632074 -7200
# Node ID 7cc3f42930f3899939f898dc7fd200816d6dca2b
# Parent  fe33d456b36c759be3a266927921a8e80993e6f9
tuned

diff -r fe33d456b36c -r 7cc3f42930f3 src/HOL/IMP/Denotational.thy
--- a/src/HOL/IMP/Denotational.thy	Wed Jun 19 10:14:50 2013 +0200
+++ b/src/HOL/IMP/Denotational.thy	Wed Jun 19 10:54:34 2013 +0200
@@ -12,7 +12,7 @@
 fun D :: "com \<Rightarrow> com_den" where
 "D SKIP   = Id" |
 "D (x ::= a) = {(s,t). t = s(x := aval a s)}" |
-"D (c0;;c1)  = D(c0) O D(c1)" |
+"D (c1;;c2)  = D(c1) O D(c2)" |
 "D (IF b THEN c1 ELSE c2)
  = {(s,t). if bval b s then (s,t) \<in> D c1 else (s,t) \<in> D c2}" |
 "D (WHILE b DO c) = lfp (W b (D c))"