# HG changeset patch
# User kleing
# Date 1014281648 -3600
# Node ID 704713ca07eada8af4431d230aa9ea3f7d8f06f6
# Parent  f5bceeec9d91f642ac39549639272852d82b0303
new document

diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -5,7 +5,7 @@
 
 *)
 
-header "The Bytecode Verifier"
+header {* \isaheader{The Bytecode Verifier}\label{sec:BVSpec} *}
 
 theory BVSpec = Effect:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "BV Type Safety Proof"
+header {* \isaheader{BV Type Safety Proof}\label{sec:BVSpecTypeSafe} *}
 
 theory BVSpecTypeSafe = Correct:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -7,7 +7,7 @@
 The invariant for the type safety proof.
 *)
 
-header "BV Type Safety Invariant"
+header {* \isaheader{BV Type Safety Invariant} *}
 
 theory Correct = BVSpec + JVMExec:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
-header {* Effect of Instructions on the State Type *}
+header {* \isaheader{Effect of Instructions on the State Type} *}
 
 theory Effect = JVMType + JVMExceptions:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
-header {* Monotonicity of eff and app *}
+header {* \isaheader{Monotonicity of eff and app} *}
 
 theory EffectMono = Effect:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -6,7 +6,7 @@
 The error type
 *)
 
-header "The Error Type"
+header {* \isaheader{The Error Type} *}
 
 theory Err = Semilat:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/JType.thy
--- a/src/HOL/MicroJava/BV/JType.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   2000 TUM
 *)
 
-header "The Java Type System as Semilattice"
+header {* \isaheader{The Java Type System as Semilattice} *}
 
 theory JType = WellForm + Err:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   2000 TUM
 *)
 
-header "Kildall for the JVM"
+header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
 
 theory JVM = Kildall_Lift + JVMType + Opt + Product + Typing_Framework_err +
              EffectMono + BVSpec:
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -5,7 +5,7 @@
 
 *)
 
-header "The JVM Type System as Semilattice"
+header {* \isaheader{The JVM Type System as Semilattice} *}
 
 theory JVMType = Opt + Product + Listn + JType:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -6,7 +6,7 @@
 Kildall's algorithm
 *)
 
-header "Kildall's Algorithm"
+header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
 
 theory Kildall = Typing_Framework + While_Combinator + Product:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
-header {* Completeness of the LBV *}
+header {* \isaheader{Completeness of the LBV} *}
 
 (* This theory is currently broken. The port to exceptions
   didn't make it into the Isabelle 2001 release. It is included for 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* Correctness of the LBV *}
+header {* \isaheader{Correctness of the LBV} *}
 
 (* This theory is currently broken. The port to exceptions
   didn't make it into the Isabelle 2001 release. It is included for 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* The Lightweight Bytecode Verifier *}
+header {* \isaheader{The Lightweight Bytecode Verifier} *}
 
 theory LBVSpec = Effect + Kildall:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -6,7 +6,7 @@
 Lists of a fixed length
 *)
 
-header "Fixed Length Lists"
+header {* \isaheader{Fixed Length Lists} *}
 
 theory Listn = Err:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Opt.thy
--- a/src/HOL/MicroJava/BV/Opt.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -6,7 +6,7 @@
 More about options
 *)
 
-header "More about Options"
+header {* \isaheader{More about Options} *}
 
 theory Opt = Err:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Product.thy
--- a/src/HOL/MicroJava/BV/Product.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -6,7 +6,7 @@
 Products as semilattices
 *)
 
-header "Products as Semilattices"
+header {* \isaheader{Products as Semilattices} *}
 
 theory Product = Err:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Semilat.thy
--- a/src/HOL/MicroJava/BV/Semilat.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -6,7 +6,10 @@
 Semilattices
 *)
 
-header "Semilattices"
+header {* 
+  \chapter{Bytecode Verifier}\label{cha:bv}
+  \isaheader{Semilattices} 
+*}
 
 theory Semilat = While_Combinator:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Typing_Framework.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   2000 TUM
 *)
 
-header "Typing and Dataflow Analysis Framework"
+header {* \isaheader{Typing and Dataflow Analysis Framework} *}
 
 theory Typing_Framework = Listn:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/BV/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -5,7 +5,7 @@
 
 *)
 
-header "Static and Dynamic Welltyping"
+header {* \isaheader{Static and Dynamic Welltyping} *}
 
 theory Typing_Framework_err = Typing_Framework:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "Conformity Relations for Type Soundness Proof"
+header {* \isaheader{Conformity Relations for Type Soundness Proof} *}
 
 theory Conform = State + WellType:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "Class Declarations and Programs"
+header {* \isaheader{Class Declarations and Programs} *}
 
 theory Decl = Type:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "Operational Evaluation (big step) Semantics"
+header {* \isaheader{Operational Evaluation (big step) Semantics} *}
 
 theory Eval = State + WellType:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "Example MicroJava Program"
+header {* \isaheader{Example MicroJava Program} *}
 
 theory Example = Eval:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/JBasis.thy
--- a/src/HOL/MicroJava/J/JBasis.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,10 @@
     Copyright   1999 TU Muenchen
 *)
 
-header "Some Auxiliary Definitions"
+header {* 
+  \chapter{Java Source Language}\label{cha:j}
+  \isaheader{Some Auxiliary Definitions}
+*}
 
 theory JBasis = Main: 
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -3,7 +3,7 @@
     Author:     Stefan Berghofer
 *)
 
-header {* Example for generating executable code from Java semantics *}
+header {* \isaheader{Example for generating executable code from Java semantics} *}
 
 theory JListExample = Eval:
 
@@ -107,7 +107,7 @@
       Expr ({list_name}(LAcc l1_name)..
         append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> _"
 
-subsection {* Big step execution *}
+section {* Big step execution *}
 
 ML {*
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "Type Safety Proof"
+header {* \isaheader{Type Safety Proof} *}
 
 theory JTypeSafe = Eval + Conform:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/State.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "Program State"
+header {* \isaheader{Program State} *}
 
 theory State = TypeRel + Value:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Term.thy
--- a/src/HOL/MicroJava/J/Term.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Term.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "Expressions and Statements"
+header {* \isaheader{Expressions and Statements} *}
 
 theory Term = Value:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Type.thy
--- a/src/HOL/MicroJava/J/Type.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Type.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "Java types"
+header {* \isaheader{Java types} *}
 
 theory Type = JBasis:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "Relations between Java Types"
+header {* \isaheader{Relations between Java Types} *}
 
 theory TypeRel = Decl:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/Value.thy
--- a/src/HOL/MicroJava/J/Value.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/Value.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "Java Values"
+header {* \isaheader{Java Values} *}
 
 theory Value = Type:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "Well-formedness of Java programs"
+header {* \isaheader{Well-formedness of Java programs} *}
 
 theory WellForm = TypeRel:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "Well-typedness Constraints"
+header {* \isaheader{Well-typedness Constraints} *}
 
 theory WellType = Term + WellForm:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/JVM/JVMExceptions.thy
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   2001 Technische Universitaet Muenchen
 *)
 
-header {* Exception handling in the JVM *}
+header {* \isaheader{Exception handling in the JVM} *}
 
 theory JVMExceptions = JVMInstructions:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/JVM/JVMExec.thy
--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* Program Execution in the JVM *}
+header {* \isaheader{Program Execution in the JVM} *}
 
 theory JVMExec = JVMExecInstr + JVMExceptions:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -5,7 +5,7 @@
 *)
 
 
-header {* JVM Instruction Semantics *}
+header {* \isaheader{JVM Instruction Semantics} *}
 
 
 theory JVMExecInstr = JVMInstructions + JVMState:
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/JVM/JVMInstructions.thy
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,7 @@
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
-header {* Instructions of the JVM *}
+header {* \isaheader{Instructions of the JVM} *}
 
 
 theory JVMInstructions = JVMState:
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -3,7 +3,7 @@
     Author:     Stefan Berghofer
 *)
 
-header {* Example for generating executable code from JVM semantics *}
+header {* \isaheader{Example for generating executable code from JVM semantics} *}
 
 theory JVMListExample = JVMExec:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/JVM/JVMState.thy
--- a/src/HOL/MicroJava/JVM/JVMState.thy	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Thu Feb 21 09:54:08 2002 +0100
@@ -4,7 +4,10 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* State of the JVM *}
+header {* 
+  \chapter{Java Virtual Machine}\label{cha:jvm}
+  \isaheader{State of the JVM} 
+*}
 
 theory JVMState = Conform:
 
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Thu Feb 21 09:54:08 2002 +0100
@@ -4,15 +4,17 @@
 add_path "JVM";
 add_path "BV";
 
+no_document use_thy "While_Combinator";
+
 use_thy "JTypeSafe";
 use_thy "Example";
 use_thy "JListExample";
 use_thy "JVMListExample";
 use_thy "BVSpecTypeSafe";
 use_thy "JVM";
-use_thy "LBVSpec"; 
 
 (* momentarily broken:
+use_thy "LBVSpec"; 
 use_thy "LBVCorrect";
 use_thy "LBVComplete";
 *)
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/document/introduction.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/document/introduction.tex	Thu Feb 21 09:54:08 2002 +0100
@@ -0,0 +1,110 @@
+
+\section*{Introduction}
+\label{sec:introduction}
+
+This document contains the automatically generated listings of the
+Isabelle sources for \mJava. \mJava{} is a reduced model of JavaCard,
+dedicated to the study of the interaction of the source language, byte
+code, the byte code verifier and the compiler. In order to make the
+Isabelle sources more accessible, this introduction provides a brief
+survey of the main concepts of \mJava.
+
+The \mJava{} \textbf{source language} (see \charef{cha:j})
+only comprises a part of the original JavaCard language. It models
+features such as:
+\begin{itemize}
+\item The basic ``primitive types'' of Java 
+\item Object orientation, in particular classes, and relevant
+  relations on classes (subclass, widening)
+
+\item Methods and method signatures
+\item Inheritance and overriding of methods, dynamic binding
+
+\item Representatives of ``relevant'' expressions and statements 
+\item Generation and propagation of system exceptions
+\end{itemize}
+
+However, the following features are missing in \mJava{} wrt.{} JavaCard:
+\begin{itemize}
+\item Some primitive types (\texttt{byte, short})
+\item Interfaces and related concepts, arrays
+\item Most numeric operations, syntactic variants of statements
+  (\texttt{do}-loop, \texttt{for}-loop)
+\item Complex block structure, method bodies with multiple returns
+\item Abrupt termination (\texttt{break, continue})
+\item Class and method modifiers (such as \texttt{static} and
+  \texttt{public/private} access modifiers)
+\item User-defined exception classes and an explicit
+  \texttt{throw}-statement. Exceptions cannot be caught.
+\item A ``definite assignment'' check
+\end{itemize}
+In addition, features are missing that are not part of the JavaCard
+language, such as multithreading and garbage collection. No attempt
+has been made to model peculiarities of JavaCard such as the applet
+firewall or the transaction mechanism.
+
+For a more complete Isabelle model of JavaCard, the reader should
+consult the Bali formalization
+(\url{http://isabelle.in.tum.de/verificard/Bali/document.pdf}), which
+models most of the source language features of JavaCard, however without
+describing the bytecode level.
+
+The central topics of the source language formalization are:
+\begin{itemize}
+\item Description of the structure of the ``runtime environment'', in
+  particular structure of classes and the program state
+\item Definition of syntax, typing rules and operational semantics of
+  statements and expressions
+\item Definition of ``conformity'' (characterizing type safety) and a
+  type safety proof
+\end{itemize}
+
+
+The \mJava{} \textbf{virtual machine} (see \charef{cha:jvm})
+corresponds rather directly to the source level, in the sense that the
+same data types are supported and bytecode instructions required for
+emulating the source level operations are provided. Again, only one
+representative of different variants of instructions has been
+selected; for example, there is only one comparison operator.  The
+formalization of the bytecode level is purely descriptive (``no
+theorems'') and rather brief as compared to the source level; all
+questions related to type systems for and type correctness of bytecode
+are dealt with in chapter on bytecode verification.
+
+The problem of \textbf{bytecode verification} (see \charef{cha:bv}) is
+dealt with in several stages:
+\begin{itemize}
+\item First, the notion of ``method type'' is introduced, which
+  corresponds to the notion of ``type'' on the source level.
+\item Well-typedness of instructions wrt. a method type is defined
+  (see \secref{sec:BVSpec}). Roughly speaking, determining
+  well-typedness is \emph{type checking}.
+\item It is shown that bytecode that is well-typed in this sense can
+  be safely executed -- a type soundness proof on the bytecode level
+  (\secref{sec:BVSpecTypeSafe}). 
+\item Given raw bytecode, one of the purposes of bytecode verification
+  is to determine a method type that is well-typed according to the
+  above definition. Roughly speaking, this is \emph{type inference}.
+  The Isabelle formalization presents bytecode verification as an
+  instance of an abstract dataflow algorithm (Kildall's algorithm, see
+  \secrefs{sec:Kildall} to \ref{sec:JVM}).
+%\item For \emph{lightweight bytecode verification}, type checking of
+%  bytecode can be reduced to method types with small size. 
+\end{itemize}
+
+Bytecode verification in \mJava{} so far takes into account:
+\begin{itemize}
+\item Operations and branching instructions
+\item Exceptions
+\end{itemize}
+Initialization during object creation is not accounted for in the
+present document 
+(see the formalization in
+\url{http://isabelle.in.tum.de/verificard/obj-init/document.pdf}),
+neither is the \texttt{jsr} instruction.
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r f5bceeec9d91 -r 704713ca07ea src/HOL/MicroJava/document/root.tex
--- a/src/HOL/MicroJava/document/root.tex	Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/document/root.tex	Thu Feb 21 09:54:08 2002 +0100
@@ -1,26 +1,36 @@
-
-\documentclass[11pt,a4paper]{article}
+%\documentclass[11pt,a4paper]{article}
+\documentclass[11pt,a4paper]{book}
 \usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup}
 
 \urlstyle{rm}
 \pagestyle{myheadings}
 
+%make a bit more space
 \addtolength{\hoffset}{-1,5cm}
 \addtolength{\textwidth}{4cm}
 \addtolength{\voffset}{-2cm}
 \addtolength{\textheight}{4cm}
 
 %subsection instead of section to make the toc readable
+\newcommand{\isaheader}[1]
+{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
 \renewcommand{\thesubsection}{\arabic{subsection}}
-\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
+\renewcommand{\isamarkupheader}[1]{#1}
 \renewcommand{\isamarkupsection}[1]{\subsubsection{#1}}
+\renewcommand{\isamarkupsubsection}[1]{\subsubsection{#1}}
 
 %remove spaces from the isabelle environment (trivlist makes them too large)
-\renewenvironment{isabelle}
-{\begin{isabellebody}}
-{\end{isabellebody}}
+%\renewenvironment{isabelle}
+%{\begin{isabellebody}}
+%{\end{isabellebody}}
+
 
 \newcommand{\mJava}{$\mu$Java}
+\newcommand{\secref}[1]{Section~\ref{#1}}
+\newcommand{\secrefs}[1]{Sections~\ref{#1}}
+\newcommand{\charef}[1]{Chapter~\ref{#1}}
+\newcommand{\charefs}[1]{Chapters~\ref{#1}}
+
 
 %remove clutter from the toc
 \setcounter{secnumdepth}{3}
@@ -28,27 +38,30 @@
 
 \begin{document}
 
-\title{\mJava}
-\author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch}
+\title{Java Source and Bytecode Formalizations in Isabelle: \mJava\\
+%  {\large -- VerifiCard Project Deliverables -- }
+}
+\author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and
+  Leonor Prensa Nieto \and Norbert Schirmer \and Martin Strecker}
 \maketitle
 
-\begin{abstract}\noindent
-  This formal development defines {\mJava}, a small fragment of the
-  programming language Java (with essentially just classes), together with a
-  corresponding virtual machine, a specification of its bytecode verifier
-  and a lightweight bytecode verifier.
-  It is shown that {\mJava} and the given specification of the bytecode
-  verifier are type-safe, and that the lightweight bytecode verifier
-  is functionally equivalent to the bytecode verifier specification.
-  See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}.
-\end{abstract}
 
 \tableofcontents
 \parindent 0pt \parskip 0.5ex
 
+\input{introduction.tex}
+
+\section*{Theory Dependencies}
+
+Figure \ref{theory-deps} shows the dependencies between 
+the Isabelle theories in the following sections.
+
+\begin{figure}
 \begin{center}
   \includegraphics[scale=0.4]{session_graph}
 \end{center}
+\caption{Theory Dependency Graph\label{theory-deps}}
+\end{figure}
 
 \newpage
 \input{session}