src/HOL/Bali/AxSem.thy
changeset 20014 729a45534001
parent 19685 4477003648cc
child 21765 89275a3ed7be
     1.1 --- a/src/HOL/Bali/AxSem.thy	Tue Jul 04 21:26:26 2006 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Wed Jul 05 11:32:38 2006 +0200
     1.3 @@ -1079,7 +1079,7 @@
     1.4  apply (rule ax_escape, clarsimp)
     1.5  apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl)
     1.6  apply (drule spec,drule spec,drule spec, erule conseq12)
     1.7 -apply (force simp add: init_lvars_def)
     1.8 +apply (force simp add: init_lvars_def Let_def)
     1.9  done
    1.10  
    1.11  lemma ax_Methd1: