# HG changeset patch
# User kleing
# Date 960390859 -7200
# Node ID 0e48e7d4d4f9a43f6759606cc5b6d3b983d58c2a
# Parent  80fca868ec4c7d1226baba349e9186dbe481716d
minor tuning for pdf documents

diff -r 80fca868ec4c -r 0e48e7d4d4f9 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Jun 07 17:14:04 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Jun 07 17:14:19 2000 +0200
@@ -2,9 +2,9 @@
     ID:         $Id$
     Author:     Gerwin Klein
     Copyright   2000 Technische Universitaet Muenchen
+*)
 
-Proof of completeness for the lightweight bytecode verifier
-*)
+header {* Completeness of the LBV *}
 
 theory LBVComplete = LBVSpec:;
 
diff -r 80fca868ec4c -r 0e48e7d4d4f9 src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Jun 07 17:14:04 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Jun 07 17:14:19 2000 +0200
@@ -2,9 +2,9 @@
     ID:         $Id$
     Author:     Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
+*)
 
-    Correctness of the lightweight bytecode verifier
-*)
+header {* Correctness of the LBV *}
 
 theory LBVCorrect = LBVSpec:;
 
diff -r 80fca868ec4c -r 0e48e7d4d4f9 src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Jun 07 17:14:04 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Jun 07 17:14:19 2000 +0200
@@ -2,9 +2,10 @@
     ID:         $Id$
     Author:     Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
+*)
 
-Specification of a lightweight bytecode verifier
-*)
+header {* Specification of the LBV *}
+
 
 theory LBVSpec = BVSpec:;
 
@@ -84,7 +85,7 @@
  wtl_CH	:: "[check_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"; 
 primrec
 "wtl_CH (Checkcast C) G s s' max_pc pc = 
-	(let (ST,LT) = s
+	(let (ST,LT) = s 
 	 in
 	 pc+1 < max_pc \\<and>
 	 is_class G C \\<and> 
@@ -221,9 +222,10 @@
     wf_prog (\\<lambda>G C (sig,rT,maxl,b). 
                wtl_method G C (snd sig) rT maxl b (cert C sig)) G"; 
 
+text {* \medskip *}
+
 lemma rev_eq: "\\<lbrakk>length a = n; length x = n; rev a @ b # c = rev x @ y # z\\<rbrakk> \\<Longrightarrow> a = x \\<and> b = y \\<and> c = z";
-proof auto;
-qed;
+by auto;
 
 lemma wtl_inst_unique: 
 "wtl_inst i G rT s0 s1 cert max_pc pc \\<longrightarrow>
@@ -244,7 +246,7 @@
   thus "wtl_inst (MI (Invoke mname list)) G rT s0 s1 cert max_pc pc \\<longrightarrow>
         wtl_inst (MI (Invoke mname list)) G rT s0 s1' cert max_pc pc \\<longrightarrow>
         s1 = s1'";
-  proof (elim);
+  proof elim;
     apply_end(clarsimp_tac, drule rev_eq, assumption+);
   qed auto;
  qed;
@@ -271,7 +273,7 @@
 
   case Cons;
   show "?P (a # list)"; 
-  proof (intro);
+  proof intro;
     fix s0; fix pc; 
     let "?o s0 s1" = "wtl_inst_option a G rT s0 s1 cert max_pc pc";
     let "?l l s1 s2 pc" = "wtl_inst_list l G rT s1 s2 cert max_pc pc";