--- 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
*)
--- 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
*)
--- 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
--- 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
*)
--- 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
*)
--- 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
*)
--- 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 *}
--- 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
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
*)
--- 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
*)
--- 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
*)
--- 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 *}
--- 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 *}
--- 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
*)
--- 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 *}
--- 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
--- 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.*}
--- 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 *}
--- 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 *}
--- 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
*)
--- 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
*)
--- 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 *}
--- 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.
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
--- 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
*)
--- 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
--- 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
*)
--- 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
--- 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
*)
--- 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 *}
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
--- 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
*)
--- 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*}
--- 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.
--- 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
--- 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.
--- 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.
--- 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 *}
--- 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.
--- 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 *}
--- 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
--- 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 *}
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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.
--- 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
*)
--- 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
*)
--- 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
--- 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
*)
--- 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
*)
--- 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
--- 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
--- 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
--- 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
--- 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
*)
--- 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
--- 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
--- 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