1.1 --- a/src/HOL/MicroJava/BV/LBVJVM.thy	Thu Apr 13 12:01:14 2006 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Thu Apr 13 12:01:15 2006 +0200
     1.3 @@ -310,7 +310,7 @@
     1.4    "wt_jvm_prog G Phi \<Longrightarrow> wt_jvm_prog_lbv G (prg_cert G Phi)"
     1.5    apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def)
     1.6    apply (erule jvm_prog_lift)
     1.7 -  apply (auto simp add: prg_cert_def intro wt_method_wt_lbv)
     1.8 +  apply (auto simp add: prg_cert_def intro: wt_method_wt_lbv)
     1.9    done  
    1.10  
    1.11  end