--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy	Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy	Fri May 17 08:19:52 2013 +0200
@@ -33,7 +33,7 @@
 fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where
 "AI SKIP S = S" |
 "AI (x ::= a) S = update S x (aval' a S)" |
-"AI (c1;c2) S = AI c2 (AI c1 S)" |
+"AI (c1;;c2) S = AI c2 (AI c1 S)" |
 "AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
 "AI (WHILE b DO c) S = pfp (AI c) S"