# HG changeset patch
# User oheimb
# Date 976208364 -3600
# Node ID d790faef9c07591fdf241229c3151e89299af96c
# Parent  4ea7f3e8e4710bd0f351ab98b5da59edd0b35c67
removed two intermediate comments

diff -r 4ea7f3e8e471 -r d790faef9c07 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Thu Dec 07 17:22:24 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Dec 07 17:59:24 2000 +0100
@@ -38,14 +38,14 @@
 "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
 by (unfold wt_jvm_prog_def, blast)
 
-lemma wt_jvm_prog_impl_wt_instr: (* DvO: is_class G C eingefügt *)
+lemma wt_jvm_prog_impl_wt_instr:
 "[| wt_jvm_prog G phi; is_class G C;
     method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] 
  ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc";
 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
     simp, simp, simp add: wf_mdecl_def wt_method_def)
 
-lemma wt_jvm_prog_impl_wt_start: (* DvO: is_class G C eingefügt *)
+lemma wt_jvm_prog_impl_wt_start:
 "[| wt_jvm_prog G phi; is_class G C;
     method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> 
  0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"