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