src/HOL/NanoJava/Equivalence.thy
changeset 51717 9e7d1c139569
parent 37604 1840dc0265da
child 58262 85b13d75b2e4
     1.1 --- a/src/HOL/NanoJava/Equivalence.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -101,7 +101,7 @@
     1.4  by(simp add: cnvalids_def nvalids_def nvalid_def2)
     1.5  
     1.6  lemma hoare_sound_main:"\<And>t. (A |\<turnstile> C \<longrightarrow> A |\<Turnstile> C) \<and> (A |\<turnstile>\<^sub>e t \<longrightarrow> A |\<Turnstile>\<^sub>e t)"
     1.7 -apply (tactic "split_all_tac 1", rename_tac P e Q)
     1.8 +apply (tactic "split_all_tac @{context} 1", rename_tac P e Q)
     1.9  apply (rule hoare_ehoare.induct)
    1.10  (*18*)
    1.11  apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})