# HG changeset patch
# User wenzelm
# Date 1144922475 -7200
# Node ID 77b19ffc175e0c9d54328a288851adc8a1e526b0
# Parent  3f5835aac3ced48cdcfa32841d082e0264ffebd3
fixed typo in method invocation;

diff -r 3f5835aac3ce -r 77b19ffc175e src/HOL/MicroJava/BV/LBVJVM.thy
--- a/src/HOL/MicroJava/BV/LBVJVM.thy	Thu Apr 13 12:01:14 2006 +0200
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Thu Apr 13 12:01:15 2006 +0200
@@ -310,7 +310,7 @@
   "wt_jvm_prog G Phi \<Longrightarrow> wt_jvm_prog_lbv G (prg_cert G Phi)"
   apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def)
   apply (erule jvm_prog_lift)
-  apply (auto simp add: prg_cert_def intro wt_method_wt_lbv)
+  apply (auto simp add: prg_cert_def intro: wt_method_wt_lbv)
   done  
 
 end