# HG changeset patch
# User wenzelm
# Date 1300053350 -3600
# Node ID b460124855b85b45ad4222e198695c2a88d93221
# Parent  5abc60a017e08c1c50fd88806b2e6099e8ec49c0
tuned headers;

diff -r 5abc60a017e0 -r b460124855b8 src/CTT/Bool.thy
--- a/src/CTT/Bool.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/CTT/Bool.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      CTT/bool
+(*  Title:      CTT/Bool.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Algebra/Congruence.thy
--- a/src/HOL/Algebra/Congruence.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Algebra/Congruence.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Algebra/Congruence.thy
+(*  Title:      HOL/Algebra/Congruence.thy
     Author:     Clemens Ballarin, started 3 January 2008
     Copyright:  Clemens Ballarin
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,9 +1,10 @@
-(*  Title:      Divisibility in monoids and rings
-    Author:     Clemens Ballarin, started 18 July 2008
-
-Based on work by Stephan Hohe.
+(*  Title:      HOL/Algebra/Divisibility.thy
+    Author:     Clemens Ballarin
+    Author:     Stephan Hohe
 *)
 
+header {* Divisibility in monoids and rings *}
+
 theory Divisibility
 imports "~~/src/HOL/Library/Permutation" Coset Group
 begin
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Algebra/Ideal.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Algebra/CIdeal.thy
+(*  Title:      HOL/Algebra/Ideal.thy
     Author:     Stephan Hohe, TU Muenchen
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Algebra/Ring.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      The algebraic hierarchy of rings
+(*  Title:      HOL/Algebra/Ring.thy
     Author:     Clemens Ballarin, started 9 December 1996
     Copyright:  Clemens Ballarin
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Univariate Polynomials
+(*  Title:      HOL/Algebra/poly/UnivPoly2.thy
     Author:     Clemens Ballarin, started 9 December 1996
     Copyright:  Clemens Ballarin
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Archimedean_Field.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,5 +1,5 @@
-(* Title:      Archimedean_Field.thy
-   Author:     Brian Huffman
+(*  Title:      HOL/Archimedean_Field.thy
+    Author:     Brian Huffman
 *)
 
 header {* Archimedean Fields, Floor and Ceiling Functions *}
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Complex.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:       Complex.thy
+(*  Title:       HOL/Complex.thy
     Author:      Jacques D. Fleuriot
     Copyright:   2001 University of Edinburgh
     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/HOLCF/Adm.thy
--- a/src/HOL/HOLCF/Adm.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/HOLCF/Adm.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Adm.thy
+(*  Title:      HOL/HOLCF/Adm.thy
     Author:     Franz Regensburger and Brian Huffman
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/HOLCF/Algebraic.thy
--- a/src/HOL/HOLCF/Algebraic.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/HOLCF/Algebraic.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Algebraic.thy
+(*  Title:      HOL/HOLCF/Algebraic.thy
     Author:     Brian Huffman
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Hoare/HeapSyntaxAbort.thy
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Hoare/HeapSyntax.thy
+(*  Title:      HOL/Hoare/HeapSyntaxAbort.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Hoare/Hoare.thy
+(*  Title:      HOL/Hoare/Hoare_Logic.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   1998 TUM
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Hoare/HoareAbort.thy
+(*  Title:      HOL/Hoare/Hoare_Logic_Abort.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   2003 TUM
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Hoare/Pointer_Examples.thy
--- a/src/HOL/Hoare/Pointer_Examples.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,8 +1,8 @@
-(*  Title:      HOL/Hoare/Pointers.thy
+(*  Title:      HOL/Hoare/Pointer_Examples.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
 
-Examples of verifications of pointer programs
+Examples of verifications of pointer programs.
 *)
 
 theory Pointer_Examples imports HeapSyntax begin
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Hoare/Pointers0.thy
--- a/src/HOL/Hoare/Pointers0.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Hoare/Pointers0.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Hoare/Pointers.thy
+(*  Title:      HOL/Hoare/Pointers0.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Hoare/SepLogHeap.thy
--- a/src/HOL/Hoare/SepLogHeap.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Hoare/SepLogHeap.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Hoare/Heap.thy
+(*  Title:      HOL/Hoare/SepLogHeap.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/IMP/Compiler0.thy
--- a/src/HOL/IMP/Compiler0.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/IMP/Compiler0.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IMP/Compiler.thy
+(*  Title:      HOL/IMP/Compiler0.thy
     Author:     Tobias Nipkow, TUM
     Copyright   1996 TUM
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/IMP/Hoare_Den.thy
--- a/src/HOL/IMP/Hoare_Den.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/IMP/Hoare_Den.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IMP/Hoare_Def.thy
+(*  Title:      HOL/IMP/Hoare_Den.thy
     Author:     Tobias Nipkow
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Induct/QuoDataType.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Induct/QuoDataType
+(*  Title:      HOL/Induct/QuoDataType.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2004  University of Cambridge
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Induct/QuoNestedDataType.thy
--- a/src/HOL/Induct/QuoNestedDataType.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Induct/QuoNestedDataType
+(*  Title:      HOL/Induct/QuoNestedDataType.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2004  University of Cambridge
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Int.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,8 +1,6 @@
-(*  Title:      Int.thy
+(*  Title:      HOL/Int.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-                Tobias Nipkow, Florian Haftmann, TU Muenchen
-    Copyright   1994  University of Cambridge
-
+    Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
 *)
 
 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Library/Bit.thy
--- a/src/HOL/Library/Bit.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Library/Bit.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,5 +1,5 @@
-(* Title:      Bit.thy
-   Author:     Brian Huffman
+(*  Title:      HOL/Library/Bit.thy
+    Author:     Brian Huffman
 *)
 
 header {* The Field of Integers mod 2 *}
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Formal_Power_Series.thy
+(*  Title:      HOL/Library/Formal_Power_Series.thy
     Author:     Amine Chaieb, University of Cambridge
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Library/Inner_Product.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,5 +1,5 @@
-(* Title:      Inner_Product.thy
-   Author:     Brian Huffman
+(*  Title:      HOL/Library/Inner_Product.thy
+    Author:     Brian Huffman
 *)
 
 header {* Inner Product Spaces and the Gradient Derivative *}
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Library/Nat_Bijection.thy
--- a/src/HOL/Library/Nat_Bijection.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Library/Nat_Bijection.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Nat_Bijection.thy
+(*  Title:      HOL/Library/Nat_Bijection.thy
     Author:     Brian Huffman
     Author:     Florian Haftmann
     Author:     Stefan Richter
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Library/Permutations.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,5 +1,5 @@
-(* Title:      Library/Permutations
-   Author:     Amine Chaieb, University of Cambridge
+(*  Title:      HOL/Library/Permutations.thy
+    Author:     Amine Chaieb, University of Cambridge
 *)
 
 header {* Permutations, both general and specifically on finite sets.*}
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Library/Poly_Deriv.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,6 +1,6 @@
-(*  Title:      Poly_Deriv.thy
+(*  Title:      HOL/Library/Poly_Deriv.thy
     Author:     Amine Chaieb
-                Ported to new Polynomial library by Brian Huffman
+    Author:     Brian Huffman
 *)
 
 header{* Polynomials and Differentiation *}
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Library/Polynomial.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,6 +1,6 @@
-(*  Title:      HOL/Polynomial.thy
+(*  Title:      HOL/Library/Polynomial.thy
     Author:     Brian Huffman
-                Based on an earlier development by Clemens Ballarin
+    Author:     Clemens Ballarin
 *)
 
 header {* Univariate Polynomials *}
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Library/RBT_Impl.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      RBT_Impl.thy
+(*  Title:      HOL/Library/RBT_Impl.thy
     Author:     Markus Reiter, TU Muenchen
     Author:     Alexander Krauss, TU Muenchen
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Ln.thy
--- a/src/HOL/Ln.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Ln.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Ln.thy
+(*  Title:      HOL/Ln.thy
     Author:     Jeremy Avigad
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Matrix/ComputeFloat.thy
--- a/src/HOL/Matrix/ComputeFloat.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Matrix/ComputeFloat.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,5 +1,5 @@
-(*  Title:  HOL/Tools/ComputeFloat.thy
-    Author: Steven Obua
+(*  Title:      HOL/Matrix/ComputeFloat.thy
+    Author:     Steven Obua
 *)
 
 header {* Floating Point Representation of the Reals *}
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Matrix/Compute_Oracle/Compute_Oracle.thy
--- a/src/HOL/Matrix/Compute_Oracle/Compute_Oracle.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/Compute_Oracle.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Tools/Compute_Oracle/Compute_Oracle.thy
+(*  Title:      HOL/Matrix/Compute_Oracle/Compute_Oracle.thy
     Author:     Steven Obua, TU Munich
 
 Steven Obua's evaluator.
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Matrix/Compute_Oracle/am_compiler.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_compiler.ML	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_compiler.ML	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Tools/Compute_Oracle/am_compiler.ML
+(*  Title:      HOL/Matrix/Compute_Oracle/am_compiler.ML
     Author:     Steven Obua
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Matrix/Compute_Oracle/am_ghc.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Tools/Compute_Oracle/am_ghc.ML
+(*  Title:      HOL/Matrix/Compute_Oracle/am_ghc.ML
     Author:     Steven Obua
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Matrix/Compute_Oracle/am_interpreter.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Tools/Compute_Oracle/am_interpreter.ML
+(*  Title:      HOL/Matrix/Compute_Oracle/am_interpreter.ML
     Author:     Steven Obua
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Matrix/Compute_Oracle/am_sml.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Tools/Compute_Oracle/am_sml.ML
+(*  Title:      HOL/Matrix/Compute_Oracle/am_sml.ML
     Author:     Steven Obua
 
 TODO: "parameterless rewrite cannot be used in pattern": In a lot of
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Matrix/Compute_Oracle/compute.ML
--- a/src/HOL/Matrix/Compute_Oracle/compute.ML	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Tools/Compute_Oracle/compute.ML
+(*  Title:      HOL/Matrix/Compute_Oracle/compute.ML
     Author:     Steven Obua
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Matrix/Compute_Oracle/linker.ML
--- a/src/HOL/Matrix/Compute_Oracle/linker.ML	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/linker.ML	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Tools/Compute_Oracle/linker.ML
+(*  Title:      HOL/Matrix/Compute_Oracle/linker.ML
     Author:     Steven Obua
 
 This module solves the problem that the computing oracle does not
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Matrix/Cplex.thy
--- a/src/HOL/Matrix/Cplex.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Matrix/Cplex.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/cplex/Cplex.thy
+(*  Title:      HOL/Matrix/Cplex.thy
     Author:     Steven Obua
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      sledgehammer_tactics.ML
+(*  Title:      HOL/Mirabelle/Tools/sledgehammer_tactics.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2010
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Convex_Euclidean_Space.thy
+(*  Title:      HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
     Author:     Robert Himmelmann, TU Muenchen
     Author:     Bogdan Grechuk, University of Edinburgh
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,5 +1,5 @@
-(* Title:      Determinants
-   Author:     Amine Chaieb, University of Cambridge
+(*  Title:      HOL/Multivariate_Analysis/Determinants.thy
+    Author:     Amine Chaieb, University of Cambridge
 *)
 
 header {* Traces, Determinant of square matrices and some properties *}
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Library/Multivariate_Analysis/Euclidean_Space.thy
+(*  Title:      HOL/Multivariate_Analysis/Euclidean_Space.thy
     Author:     Amine Chaieb, University of Cambridge
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Multivariate_Analysis/L2_Norm.thy
--- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Multivariate_Analysis/L2_Norm.thy
+(*  Title:      HOL/Multivariate_Analysis/L2_Norm.thy
     Author:     Brian Huffman, Portland State University
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Multivariate_Analysis/Operator_Norm.thy
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Library/Operator_Norm.thy
+(*  Title:      HOL/Multivariate_Analysis/Operator_Norm.thy
     Author:     Amine Chaieb, University of Cambridge
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Multivariate_Analysis/Path_Connected.thy
+(*  Title:      HOL/Multivariate_Analysis/Path_Connected.thy
     Author:     Robert Himmelmann, TU Muenchen
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/NSA/Filter.thy
--- a/src/HOL/NSA/Filter.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/NSA/Filter.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Filter.thy
+(*  Title:      HOL/NSA/Filter.thy
     Author:     Jacques D. Fleuriot, University of Cambridge
     Author:     Lawrence C Paulson
     Author:     Brian Huffman
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/NSA/HLim.thy
--- a/src/HOL/NSA/HLim.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/NSA/HLim.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HLim.thy
+(*  Title:      HOL/NSA/HLim.thy
     Author:     Jacques D. Fleuriot, University of Cambridge
     Author:     Lawrence C Paulson
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/NSA/NSComplex.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,7 +1,6 @@
-(*  Title:       NSComplex.thy
-    Author:      Jacques D. Fleuriot
-    Copyright:   2001  University of Edinburgh
-    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
+(*  Title:      HOL/NSA/NSComplex.thy
+    Author:     Jacques D. Fleuriot, University of Edinburgh
+    Author:     Lawrence C Paulson
 *)
 
 header{*Nonstandard Complex Numbers*}
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Binomial.thy
+(*  Title:      HOL/Number_Theory/Binomial.thy
     Authors:    Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
 
 Defines the "choose" function, and establishes basic properties.
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Cong.thy
+(*  Title:      HOL/Number_Theory/Cong.thy
     Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
                 Thomas M. Rasmussen, Jeremy Avigad
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Number_Theory/Fib.thy
--- a/src/HOL/Number_Theory/Fib.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Number_Theory/Fib.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,5 +1,6 @@
-(*  Title:      Fib.thy
-    Authors:    Lawrence C. Paulson, Jeremy Avigad
+(*  Title:      HOL/Number_Theory/Fib.thy
+    Author:     Lawrence C. Paulson
+    Author:     Jeremy Avigad
 
 Defines the fibonacci function.
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Number_Theory/MiscAlgebra.thy
--- a/src/HOL/Number_Theory/MiscAlgebra.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      MiscAlgebra.thy
+(*  Title:      HOL/Number_Theory/MiscAlgebra.thy
     Author:     Jeremy Avigad
 
 These are things that can be added to the Algebra library.
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,8 +1,8 @@
-(*  Title:      HOL/Library/Residues.thy
+(*  Title:      HOL/Number_Theory/Residues.thy
     Author:     Jeremy Avigad
 
 An algebraic treatment of residue rings, and resulting proofs of
-Euler's theorem and Wilson's theorem. 
+Euler's theorem and Wilson's theorem.
 *)
 
 header {* Residue rings *}
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      UniqueFactorization.thy
+(*  Title:      HOL/Number_Theory/UniqueFactorization.thy
     Author:     Jeremy Avigad
 
 Unique factorization for the natural numbers and the integers.
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Parity.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,5 +1,6 @@
-(*  Title:      HOL/Library/Parity.thy
-    Author:     Jeremy Avigad, Jacques D. Fleuriot
+(*  Title:      HOL/Parity.thy
+    Author:     Jeremy Avigad
+    Author:     Jacques D. Fleuriot
 *)
 
 header {* Even and Odd for int and nat *}
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Probability/Complete_Measure.thy
--- a/src/HOL/Probability/Complete_Measure.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,6 +1,7 @@
-(*  Title:      Complete_Measure.thy
+(*  Title:      HOL/Probability/Complete_Measure.thy
     Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
 *)
+
 theory Complete_Measure
 imports Product_Measure
 begin
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,7 +1,7 @@
-(*  Title:      Sigma_Algebra.thy
-    Author:     Stefan Richter, Markus Wenzel, TU Muenchen
-    Plus material from the Hurd/Coble measure theory development,
-    translated by Lawrence Paulson.
+(*  Title:      HOL/Probability/Sigma_Algebra.thy
+    Author:     Stefan Richter
+    Author:     Markus Wenzel
+    Author:     Lawrence Paulson
 *)
 
 header {* Sigma Algebras *}
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Quotient.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Quotient.thy
+(*  Title:      HOL/Quotient.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Statespace/StateFun.thy
--- a/src/HOL/Statespace/StateFun.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Statespace/StateFun.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      StateFun.thy
+(*  Title:      HOL/Statespace/StateFun.thy
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Statespace/StateSpaceEx.thy
--- a/src/HOL/Statespace/StateSpaceEx.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      StateSpaceEx.thy
+(*  Title:      HOL/Statespace/StateSpaceEx.thy
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Statespace/StateSpaceLocale.thy
--- a/src/HOL/Statespace/StateSpaceLocale.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      StateSpaceLocale.thy
+(*  Title:      HOL/Statespace/StateSpaceLocale.thy
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Statespace/StateSpaceSyntax.thy
--- a/src/HOL/Statespace/StateSpaceSyntax.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      StateSpaceSyntax.thy
+(*  Title:      HOL/Statespace/StateSpaceSyntax.thy
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/Word/Tools/smt_word.ML
--- a/src/HOL/Word/Tools/smt_word.ML	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Word/Tools/smt_word.ML	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/SMT/smt_word.ML
+(*  Title:      HOL/Word/Tools/smt_word.ML
     Author:     Sascha Boehme, TU Muenchen
 
 SMT setup for words.
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/ex/Arithmetic_Series_Complex.thy
--- a/src/HOL/ex/Arithmetic_Series_Complex.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/ex/Arithmetic_Series_Complex.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/Arithmetic_Series_Complex
+(*  Title:      HOL/ex/Arithmetic_Series_Complex.thy
     Author:     Benjamin Porter, 2006
 *)
 
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/ex/Classical.thy
--- a/src/HOL/ex/Classical.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/ex/Classical.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/Classical
+(*  Title:      HOL/ex/Classical.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/ex/CodegenSML_Test.thy
--- a/src/HOL/ex/CodegenSML_Test.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/ex/CodegenSML_Test.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,5 +1,7 @@
-(*  Title:      Test file for Stefan Berghofer's SML code generator
+(*  Title:      HOL/ex/CodegenSML_Test.thy
     Author:     Tobias Nipkow, TU Muenchen
+
+Test file for Stefan Berghofer's SML code generator.
 *)
 
 theory CodegenSML_Test
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/ex/Sorting.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/sorting.thy
+(*  Title:      HOL/ex/Sorting.thy
     Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/HOL/ex/While_Combinator_Example.thy
--- a/src/HOL/ex/While_Combinator_Example.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/ex/While_Combinator_Example.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/While_Combinator.thy
+(*  Title:      HOL/ex/While_Combinator_Example.thy
     Author:     Tobias Nipkow
     Copyright   2000 TU Muenchen
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/Pure/Isar/generic_target.ML	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Pure/Isar/theory_target.ML
+(*  Title:      Pure/Isar/generic_target.ML
     Author:     Makarius
     Author:     Florian Haftmann, TU Muenchen
 
diff -r 5abc60a017e0 -r b460124855b8 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/Pure/Isar/named_target.ML	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Pure/Isar/theory_target.ML
+(*  Title:      Pure/Isar/named_target.ML
     Author:     Makarius
     Author:     Florian Haftmann, TU Muenchen
 
diff -r 5abc60a017e0 -r b460124855b8 src/Sequents/LK.thy
--- a/src/Sequents/LK.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/Sequents/LK.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      LK/LK.ML
+(*  Title:      Sequents/LK.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
diff -r 5abc60a017e0 -r b460124855b8 src/Sequents/LK/Hard_Quantifiers.thy
--- a/src/Sequents/LK/Hard_Quantifiers.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/Sequents/LK/Hard_Quantifiers.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      LK/Hard_Quantifiers.thy
+(*  Title:      Sequents/LK/Hard_Quantifiers.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
diff -r 5abc60a017e0 -r b460124855b8 src/Sequents/LK/Propositional.thy
--- a/src/Sequents/LK/Propositional.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/Sequents/LK/Propositional.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      LK/Propositional.thy
+(*  Title:      Sequents/LK/Propositional.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
diff -r 5abc60a017e0 -r b460124855b8 src/Sequents/LK/Quantifiers.thy
--- a/src/Sequents/LK/Quantifiers.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/Sequents/LK/Quantifiers.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      LK/Quantifiers.thy
+(*  Title:      Sequents/LK/Quantifiers.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
diff -r 5abc60a017e0 -r b460124855b8 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/Sequents/LK0.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      LK/LK0.thy
+(*  Title:      Sequents/LK0.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
diff -r 5abc60a017e0 -r b460124855b8 src/Sequents/S43.thy
--- a/src/Sequents/S43.thy	Sun Mar 13 22:24:10 2011 +0100
+++ b/src/Sequents/S43.thy	Sun Mar 13 22:55:50 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Modal/S43.thy
+(*  Title:      Sequents/S43.thy
     Author:     Martin Coen
     Copyright   1991  University of Cambridge