--- a/src/HOL/MicroJava/BV/BVSpec.thy Fri Jul 25 12:03:28 2008 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Fri Jul 25 12:03:31 2008 +0200
@@ -7,7 +7,9 @@
header {* \isaheader{The Bytecode Verifier}\label{sec:BVSpec} *}
-theory BVSpec imports Effect begin
+theory BVSpec
+imports Effect
+begin
text {*
This theory contains a specification of the BV. The specification
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Jul 25 12:03:28 2008 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Jul 25 12:03:31 2008 +0200
@@ -6,7 +6,9 @@
header {* \isaheader{BV Type Safety Proof}\label{sec:BVSpecTypeSafe} *}
-theory BVSpecTypeSafe imports Correct begin
+theory BVSpecTypeSafe
+imports Correct
+begin
text {*
This theory contains proof that the specification of the bytecode
--- a/src/HOL/MicroJava/BV/Opt.thy Fri Jul 25 12:03:28 2008 +0200
+++ b/src/HOL/MicroJava/BV/Opt.thy Fri Jul 25 12:03:31 2008 +0200
@@ -8,7 +8,9 @@
header {* \isaheader{More about Options} *}
-theory Opt imports Err begin
+theory Opt
+imports Err
+begin
constdefs
le :: "'a ord \<Rightarrow> 'a option ord"
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy Fri Jul 25 12:03:28 2008 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy Fri Jul 25 12:03:31 2008 +0200
@@ -6,7 +6,9 @@
header {* \isaheader{Typing and Dataflow Analysis Framework} *}
-theory Typing_Framework imports Listn begin
+theory Typing_Framework
+imports Listn
+begin
text {*
The relationship between dataflow analysis and a welltyped-instruction predicate.
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy Fri Jul 25 12:03:28 2008 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy Fri Jul 25 12:03:31 2008 +0200
@@ -7,7 +7,9 @@
header {* \isaheader{Lifting the Typing Framework to err, app, and eff} *}
-theory Typing_Framework_err imports Typing_Framework SemilatAlg begin
+theory Typing_Framework_err
+imports Typing_Framework SemilatAlg
+begin
constdefs
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/MicroJava.thy Fri Jul 25 12:03:31 2008 +0200
@@ -0,0 +1,15 @@
+theory MicroJava
+imports
+ "J/JTypeSafe"
+ "J/Example"
+ "J/JListExample"
+ "JVM/JVMListExample"
+ "JVM/JVMDefensive"
+ "BV/LBVJVM"
+ "BV/BVNoTypeError"
+ "BV/BVExample"
+ "Comp/CorrComp"
+ "Comp/CorrCompTp"
+begin
+
+end
\ No newline at end of file
--- a/src/HOL/MicroJava/ROOT.ML Fri Jul 25 12:03:28 2008 +0200
+++ b/src/HOL/MicroJava/ROOT.ML Fri Jul 25 12:03:31 2008 +0200
@@ -2,7 +2,4 @@
no_document use_thy "While_Combinator";
-use_thys ["J/JTypeSafe", "J/Example", "J/JListExample",
- "JVM/JVMListExample", "JVM/JVMDefensive", "BV/LBVJVM",
- "BV/BVNoTypeError", "BV/BVExample", "Comp/CorrComp",
- "Comp/CorrCompTp"];
+use_thy "MicroJava";