# HG changeset patch
# User kleing
# Date 976037761 -3600
# Node ID 3288024b4d437c139c33a220217a96d0e96c5072
# Parent  fc0b575a2cf7ebac949a3986e5cb0c07c36ce928
fixed document preparation

diff -r fc0b575a2cf7 -r 3288024b4d43 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Tue Dec 05 14:08:56 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Tue Dec 05 18:36:01 2000 +0100
@@ -50,7 +50,7 @@
 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
     simp, simp add: wf_mdecl_def wt_method_def)
 
-text "for most instructions wt_instr collapses:"
+text {* for most instructions wt\_instr collapses: *}
 lemma  
 "succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc = 
  (app i G mxs rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"