tuned headers;
authorwenzelm
Tue, 29 Mar 2011 17:30:26 +0200
changeset 42150 b0c0638c4aad
parent 42149 7e6f4ca198bb
child 42151 4da4fc77664b
tuned headers;
src/HOL/MicroJava/BV/BVNoTypeError.thy
src/HOL/MicroJava/BV/EffectMono.thy
src/HOL/MicroJava/BV/JVMType.thy
src/HOL/MicroJava/BV/LBVJVM.thy
src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
src/HOL/MicroJava/DFA/Abstract_BV.thy
src/HOL/MicroJava/DFA/Err.thy
src/HOL/MicroJava/DFA/Kildall.thy
src/HOL/MicroJava/DFA/LBVComplete.thy
src/HOL/MicroJava/DFA/LBVSpec.thy
src/HOL/MicroJava/DFA/Listn.thy
src/HOL/MicroJava/DFA/Opt.thy
src/HOL/MicroJava/DFA/Product.thy
src/HOL/MicroJava/DFA/Semilat.thy
src/HOL/MicroJava/DFA/SemilatAlg.thy
src/HOL/MicroJava/DFA/Semilattices.thy
src/HOL/MicroJava/DFA/Typing_Framework.thy
src/HOL/MicroJava/DFA/Typing_Framework_err.thy
src/HOL/Probability/Borel_Space.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
 *)
 
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)