# HG changeset patch
# User haftmann
# Date 1216980211 -7200
# Node ID 5a557a5afc48b14dfa97d5c47c8c9274ad814b89
# Parent  6392b92c3536fac8f8720a4df3246685eb417674
added explicit root theory; some tuning

diff -r 6392b92c3536 -r 5a557a5afc48 src/HOL/MicroJava/BV/BVSpec.thy
--- 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
diff -r 6392b92c3536 -r 5a557a5afc48 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- 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
diff -r 6392b92c3536 -r 5a557a5afc48 src/HOL/MicroJava/BV/Opt.thy
--- 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"
diff -r 6392b92c3536 -r 5a557a5afc48 src/HOL/MicroJava/BV/Typing_Framework.thy
--- 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. 
diff -r 6392b92c3536 -r 5a557a5afc48 src/HOL/MicroJava/BV/Typing_Framework_err.thy
--- 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
 
diff -r 6392b92c3536 -r 5a557a5afc48 src/HOL/MicroJava/MicroJava.thy
--- /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
diff -r 6392b92c3536 -r 5a557a5afc48 src/HOL/MicroJava/ROOT.ML
--- 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";