src/HOL/IMP/Comp_Rev.thy

 
 lemma ccomp_empty [elim!]:
   "ccomp c = [] \<Longrightarrow> (c,s) \<Rightarrow> s"
   by (induct c) auto
 
-lemma assign [simp]:
-  "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
-  by auto
+declare assign_simp [simp]
 
 lemma ccomp_exec_n:
   "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (isize(ccomp c),t,stk')
   \<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk"
 proof (induct c arbitrary: s t stk stk' n)