--- a/src/HOL/Bali/AxSound.thy Wed Jan 12 17:14:27 2011 +0100
+++ b/src/HOL/Bali/AxSound.thy Wed Jan 12 17:19:50 2011 +0100
@@ -293,7 +293,7 @@
and da: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>C"
and elim: "\<lbrakk>Q v s1 Z; s1\<Colon>\<preceq>(G,L)\<rbrakk> \<Longrightarrow> concl"
shows concl
-using prems
+using assms
by (simp add: ax_valids2_def triple_valid2_def2) fast
(* why consumes 5?. If I want to apply this lemma in a context wgere
\<not> normal s0 holds,