# HG changeset patch
# User wenzelm
# Date 1301412626 -7200
# Node ID b0c0638c4aad0ba5e436fb4745b3bc8d59ae1e7a
# Parent  7e6f4ca198bba9d9c53de7d285356bec520aae30
tuned headers;

diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/BVNoTypeErrors.thy
+(*  Title:      HOL/MicroJava/BV/BVNoTypeError.thy
     Author:     Gerwin Klein
 *)
 
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/EffMono.thy
+(*  Title:      HOL/MicroJava/BV/EffectMono.thy
     Author:     Gerwin Klein
     Copyright   2000 Technische Universitaet Muenchen
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/JVM.thy
+(*  Title:      HOL/MicroJava/BV/JVMType.thy
     Author:     Gerwin Klein
     Copyright   2000 TUM
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/BV/LBVJVM.thy
--- a/src/HOL/MicroJava/BV/LBVJVM.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/JVM.thy
+(*  Title:      HOL/MicroJava/BV/LBVJVM.thy
     Author:     Tobias Nipkow, Gerwin Klein
     Copyright   2000 TUM
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/JVM.thy
+(*  Title:      HOL/MicroJava/BV/Typing_Framework_JVM.thy
     Author:     Tobias Nipkow, Gerwin Klein
     Copyright   2000 TUM
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/DFA/Abstract_BV.thy
--- a/src/HOL/MicroJava/DFA/Abstract_BV.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Abstract_BV.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/Semilat.thy
+(*  Title:      HOL/MicroJava/DFA/Abstract_BV.thy
     Author:     Gerwin Klein
     Copyright   2003 TUM
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/DFA/Err.thy
--- a/src/HOL/MicroJava/DFA/Err.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Err.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/Err.thy
+(*  Title:      HOL/MicroJava/DFA/Err.thy
     Author:     Tobias Nipkow
     Copyright   2000 TUM
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/Kildall.thy
+(*  Title:      HOL/MicroJava/DFA/Kildall.thy
     Author:     Tobias Nipkow, Gerwin Klein
     Copyright   2000 TUM
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/DFA/LBVComplete.thy
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/LBVComplete.thy
+(*  Title:      HOL/MicroJava/DFA/LBVComplete.thy
     Author:     Gerwin Klein
     Copyright   2000 Technische Universitaet Muenchen
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/DFA/LBVSpec.thy
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/LBVSpec.thy
+(*  Title:      HOL/MicroJava/DFA/LBVSpec.thy
     Author:     Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/DFA/Listn.thy
--- a/src/HOL/MicroJava/DFA/Listn.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Listn.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/Listn.thy
+(*  Title:      HOL/MicroJava/DFA/Listn.thy
     Author:     Tobias Nipkow
     Copyright   2000 TUM
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/DFA/Opt.thy
--- a/src/HOL/MicroJava/DFA/Opt.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Opt.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/Opt.thy
+(*  Title:      HOL/MicroJava/DFA/Opt.thy
     Author:     Tobias Nipkow
     Copyright   2000 TUM
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/DFA/Product.thy
--- a/src/HOL/MicroJava/DFA/Product.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Product.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/Product.thy
+(*  Title:      HOL/MicroJava/DFA/Product.thy
     Author:     Tobias Nipkow
     Copyright   2000 TUM
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/DFA/Semilat.thy
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/Semilat.thy
+(*  Title:      HOL/MicroJava/DFA/Semilat.thy
     Author:     Tobias Nipkow
     Copyright   2000 TUM
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/DFA/SemilatAlg.thy
--- a/src/HOL/MicroJava/DFA/SemilatAlg.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/SemilatAlg.thy
+(*  Title:      HOL/MicroJava/DFA/SemilatAlg.thy
     Author:     Gerwin Klein
     Copyright   2002 Technische Universitaet Muenchen
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/DFA/Semilattices.thy
--- a/src/HOL/MicroJava/DFA/Semilattices.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Semilattices.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/Semilat.thy
+(*  Title:      HOL/MicroJava/DFA/Semilattices.thy
     Author:     Gerwin Klein
     Copyright   2003 TUM
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/DFA/Typing_Framework.thy
--- a/src/HOL/MicroJava/DFA/Typing_Framework.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Typing_Framework.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/Typing_Framework.thy
+(*  Title:      HOL/MicroJava/DFA/Typing_Framework.thy
     Author:     Tobias Nipkow
     Copyright   2000 TUM
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/MicroJava/DFA/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/DFA/Typing_Framework_err.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Typing_Framework_err.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/Typing_Framework_err.thy
+(*  Title:      HOL/MicroJava/DFA/Typing_Framework_err.thy
     Author:     Gerwin Klein
     Copyright   2000 TUM
 *)
diff -r 7e6f4ca198bb -r b0c0638c4aad src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Tue Mar 29 14:27:44 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Tue Mar 29 17:30:26 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Probability/Lebesgue_Integration.thy
+(*  Title:      HOL/Probability/Borel_Space.thy
     Author:     Johannes Hölzl, TU München
     Author:     Armin Heller, TU München
 *)