src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy

 
 
 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"
 
 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
 proof(induction c arbitrary: s t S0)