diff -r 8d5221bf765b -r 1f99296758c2 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Tue Aug 08 16:57:44 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Wed Aug 09 11:53:00 2000 +0200
@@ -36,6 +36,8 @@
    wf_prog (\\<lambda>G C (sig,rT,maxl,b).
               wt_method G C (snd sig) rT maxl b (phi C sig)) G"
 
+
+
 lemma wt_jvm_progD:
 "wt_jvm_prog G phi \\<Longrightarrow> (\\<exists>wt. wf_prog wt G)"
 by (unfold wt_jvm_prog_def, blast)