tuned headers;
authorwenzelm
Sun Mar 13 22:55:50 2011 +0100 (2011-03-13)
changeset 41959b460124855b8
parent 41958 5abc60a017e0
child 41960 8a399da4cde1
tuned headers;
src/CTT/Bool.thy
src/HOL/Algebra/Congruence.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Archimedean_Field.thy
src/HOL/Complex.thy
src/HOL/HOLCF/Adm.thy
src/HOL/HOLCF/Algebraic.thy
src/HOL/Hoare/HeapSyntaxAbort.thy
src/HOL/Hoare/Hoare_Logic.thy
src/HOL/Hoare/Hoare_Logic_Abort.thy
src/HOL/Hoare/Pointer_Examples.thy
src/HOL/Hoare/Pointers0.thy
src/HOL/Hoare/SepLogHeap.thy
src/HOL/IMP/Compiler0.thy
src/HOL/IMP/Hoare_Den.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Int.thy
src/HOL/Library/Bit.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Nat_Bijection.thy
src/HOL/Library/Permutations.thy
src/HOL/Library/Poly_Deriv.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Ln.thy
src/HOL/Matrix/ComputeFloat.thy
src/HOL/Matrix/Compute_Oracle/Compute_Oracle.thy
src/HOL/Matrix/Compute_Oracle/am_compiler.ML
src/HOL/Matrix/Compute_Oracle/am_ghc.ML
src/HOL/Matrix/Compute_Oracle/am_interpreter.ML
src/HOL/Matrix/Compute_Oracle/am_sml.ML
src/HOL/Matrix/Compute_Oracle/compute.ML
src/HOL/Matrix/Compute_Oracle/linker.ML
src/HOL/Matrix/Cplex.thy
src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Determinants.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/L2_Norm.thy
src/HOL/Multivariate_Analysis/Operator_Norm.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/NSA/Filter.thy
src/HOL/NSA/HLim.thy
src/HOL/NSA/NSComplex.thy
src/HOL/Number_Theory/Binomial.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Fib.thy
src/HOL/Number_Theory/MiscAlgebra.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Parity.thy
src/HOL/Probability/Complete_Measure.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Quotient.thy
src/HOL/Statespace/StateFun.thy
src/HOL/Statespace/StateSpaceEx.thy
src/HOL/Statespace/StateSpaceLocale.thy
src/HOL/Statespace/StateSpaceSyntax.thy
src/HOL/Word/Tools/smt_word.ML
src/HOL/ex/Arithmetic_Series_Complex.thy
src/HOL/ex/Classical.thy
src/HOL/ex/CodegenSML_Test.thy
src/HOL/ex/Sorting.thy
src/HOL/ex/While_Combinator_Example.thy
src/Pure/Isar/generic_target.ML
src/Pure/Isar/named_target.ML
src/Sequents/LK.thy
src/Sequents/LK/Hard_Quantifiers.thy
src/Sequents/LK/Propositional.thy
src/Sequents/LK/Quantifiers.thy
src/Sequents/LK0.thy
src/Sequents/S43.thy
     1.1 --- a/src/CTT/Bool.thy	Sun Mar 13 22:24:10 2011 +0100
     1.2 +++ b/src/CTT/Bool.thy	Sun Mar 13 22:55:50 2011 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      CTT/bool
     1.5 +(*  Title:      CTT/Bool.thy
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1991  University of Cambridge
     1.8  *)
     2.1 --- a/src/HOL/Algebra/Congruence.thy	Sun Mar 13 22:24:10 2011 +0100
     2.2 +++ b/src/HOL/Algebra/Congruence.thy	Sun Mar 13 22:55:50 2011 +0100
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      Algebra/Congruence.thy
     2.5 +(*  Title:      HOL/Algebra/Congruence.thy
     2.6      Author:     Clemens Ballarin, started 3 January 2008
     2.7      Copyright:  Clemens Ballarin
     2.8  *)
     3.1 --- a/src/HOL/Algebra/Divisibility.thy	Sun Mar 13 22:24:10 2011 +0100
     3.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sun Mar 13 22:55:50 2011 +0100
     3.3 @@ -1,9 +1,10 @@
     3.4 -(*  Title:      Divisibility in monoids and rings
     3.5 -    Author:     Clemens Ballarin, started 18 July 2008
     3.6 -
     3.7 -Based on work by Stephan Hohe.
     3.8 +(*  Title:      HOL/Algebra/Divisibility.thy
     3.9 +    Author:     Clemens Ballarin
    3.10 +    Author:     Stephan Hohe
    3.11  *)
    3.12  
    3.13 +header {* Divisibility in monoids and rings *}
    3.14 +
    3.15  theory Divisibility
    3.16  imports "~~/src/HOL/Library/Permutation" Coset Group
    3.17  begin
     4.1 --- a/src/HOL/Algebra/Ideal.thy	Sun Mar 13 22:24:10 2011 +0100
     4.2 +++ b/src/HOL/Algebra/Ideal.thy	Sun Mar 13 22:55:50 2011 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/Algebra/CIdeal.thy
     4.5 +(*  Title:      HOL/Algebra/Ideal.thy
     4.6      Author:     Stephan Hohe, TU Muenchen
     4.7  *)
     4.8  
     5.1 --- a/src/HOL/Algebra/Ring.thy	Sun Mar 13 22:24:10 2011 +0100
     5.2 +++ b/src/HOL/Algebra/Ring.thy	Sun Mar 13 22:55:50 2011 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      The algebraic hierarchy of rings
     5.5 +(*  Title:      HOL/Algebra/Ring.thy
     5.6      Author:     Clemens Ballarin, started 9 December 1996
     5.7      Copyright:  Clemens Ballarin
     5.8  *)
     6.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Sun Mar 13 22:24:10 2011 +0100
     6.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Sun Mar 13 22:55:50 2011 +0100
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      Univariate Polynomials
     6.5 +(*  Title:      HOL/Algebra/poly/UnivPoly2.thy
     6.6      Author:     Clemens Ballarin, started 9 December 1996
     6.7      Copyright:  Clemens Ballarin
     6.8  *)
     7.1 --- a/src/HOL/Archimedean_Field.thy	Sun Mar 13 22:24:10 2011 +0100
     7.2 +++ b/src/HOL/Archimedean_Field.thy	Sun Mar 13 22:55:50 2011 +0100
     7.3 @@ -1,5 +1,5 @@
     7.4 -(* Title:      Archimedean_Field.thy
     7.5 -   Author:     Brian Huffman
     7.6 +(*  Title:      HOL/Archimedean_Field.thy
     7.7 +    Author:     Brian Huffman
     7.8  *)
     7.9  
    7.10  header {* Archimedean Fields, Floor and Ceiling Functions *}
     8.1 --- a/src/HOL/Complex.thy	Sun Mar 13 22:24:10 2011 +0100
     8.2 +++ b/src/HOL/Complex.thy	Sun Mar 13 22:55:50 2011 +0100
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:       Complex.thy
     8.5 +(*  Title:       HOL/Complex.thy
     8.6      Author:      Jacques D. Fleuriot
     8.7      Copyright:   2001 University of Edinburgh
     8.8      Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
     9.1 --- a/src/HOL/HOLCF/Adm.thy	Sun Mar 13 22:24:10 2011 +0100
     9.2 +++ b/src/HOL/HOLCF/Adm.thy	Sun Mar 13 22:55:50 2011 +0100
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      HOLCF/Adm.thy
     9.5 +(*  Title:      HOL/HOLCF/Adm.thy
     9.6      Author:     Franz Regensburger and Brian Huffman
     9.7  *)
     9.8  
    10.1 --- a/src/HOL/HOLCF/Algebraic.thy	Sun Mar 13 22:24:10 2011 +0100
    10.2 +++ b/src/HOL/HOLCF/Algebraic.thy	Sun Mar 13 22:55:50 2011 +0100
    10.3 @@ -1,4 +1,4 @@
    10.4 -(*  Title:      HOLCF/Algebraic.thy
    10.5 +(*  Title:      HOL/HOLCF/Algebraic.thy
    10.6      Author:     Brian Huffman
    10.7  *)
    10.8  
    11.1 --- a/src/HOL/Hoare/HeapSyntaxAbort.thy	Sun Mar 13 22:24:10 2011 +0100
    11.2 +++ b/src/HOL/Hoare/HeapSyntaxAbort.thy	Sun Mar 13 22:55:50 2011 +0100
    11.3 @@ -1,4 +1,4 @@
    11.4 -(*  Title:      HOL/Hoare/HeapSyntax.thy
    11.5 +(*  Title:      HOL/Hoare/HeapSyntaxAbort.thy
    11.6      Author:     Tobias Nipkow
    11.7      Copyright   2002 TUM
    11.8  *)
    12.1 --- a/src/HOL/Hoare/Hoare_Logic.thy	Sun Mar 13 22:24:10 2011 +0100
    12.2 +++ b/src/HOL/Hoare/Hoare_Logic.thy	Sun Mar 13 22:55:50 2011 +0100
    12.3 @@ -1,4 +1,4 @@
    12.4 -(*  Title:      HOL/Hoare/Hoare.thy
    12.5 +(*  Title:      HOL/Hoare/Hoare_Logic.thy
    12.6      Author:     Leonor Prensa Nieto & Tobias Nipkow
    12.7      Copyright   1998 TUM
    12.8  
    13.1 --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Sun Mar 13 22:24:10 2011 +0100
    13.2 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Sun Mar 13 22:55:50 2011 +0100
    13.3 @@ -1,4 +1,4 @@
    13.4 -(*  Title:      HOL/Hoare/HoareAbort.thy
    13.5 +(*  Title:      HOL/Hoare/Hoare_Logic_Abort.thy
    13.6      Author:     Leonor Prensa Nieto & Tobias Nipkow
    13.7      Copyright   2003 TUM
    13.8  
    14.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Sun Mar 13 22:24:10 2011 +0100
    14.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Sun Mar 13 22:55:50 2011 +0100
    14.3 @@ -1,8 +1,8 @@
    14.4 -(*  Title:      HOL/Hoare/Pointers.thy
    14.5 +(*  Title:      HOL/Hoare/Pointer_Examples.thy
    14.6      Author:     Tobias Nipkow
    14.7      Copyright   2002 TUM
    14.8  
    14.9 -Examples of verifications of pointer programs
   14.10 +Examples of verifications of pointer programs.
   14.11  *)
   14.12  
   14.13  theory Pointer_Examples imports HeapSyntax begin
    15.1 --- a/src/HOL/Hoare/Pointers0.thy	Sun Mar 13 22:24:10 2011 +0100
    15.2 +++ b/src/HOL/Hoare/Pointers0.thy	Sun Mar 13 22:55:50 2011 +0100
    15.3 @@ -1,4 +1,4 @@
    15.4 -(*  Title:      HOL/Hoare/Pointers.thy
    15.5 +(*  Title:      HOL/Hoare/Pointers0.thy
    15.6      Author:     Tobias Nipkow
    15.7      Copyright   2002 TUM
    15.8  
    16.1 --- a/src/HOL/Hoare/SepLogHeap.thy	Sun Mar 13 22:24:10 2011 +0100
    16.2 +++ b/src/HOL/Hoare/SepLogHeap.thy	Sun Mar 13 22:55:50 2011 +0100
    16.3 @@ -1,4 +1,4 @@
    16.4 -(*  Title:      HOL/Hoare/Heap.thy
    16.5 +(*  Title:      HOL/Hoare/SepLogHeap.thy
    16.6      Author:     Tobias Nipkow
    16.7      Copyright   2002 TUM
    16.8  
    17.1 --- a/src/HOL/IMP/Compiler0.thy	Sun Mar 13 22:24:10 2011 +0100
    17.2 +++ b/src/HOL/IMP/Compiler0.thy	Sun Mar 13 22:55:50 2011 +0100
    17.3 @@ -1,4 +1,4 @@
    17.4 -(*  Title:      HOL/IMP/Compiler.thy
    17.5 +(*  Title:      HOL/IMP/Compiler0.thy
    17.6      Author:     Tobias Nipkow, TUM
    17.7      Copyright   1996 TUM
    17.8  
    18.1 --- a/src/HOL/IMP/Hoare_Den.thy	Sun Mar 13 22:24:10 2011 +0100
    18.2 +++ b/src/HOL/IMP/Hoare_Den.thy	Sun Mar 13 22:55:50 2011 +0100
    18.3 @@ -1,4 +1,4 @@
    18.4 -(*  Title:      HOL/IMP/Hoare_Def.thy
    18.5 +(*  Title:      HOL/IMP/Hoare_Den.thy
    18.6      Author:     Tobias Nipkow
    18.7  *)
    18.8  
    19.1 --- a/src/HOL/Induct/QuoDataType.thy	Sun Mar 13 22:24:10 2011 +0100
    19.2 +++ b/src/HOL/Induct/QuoDataType.thy	Sun Mar 13 22:55:50 2011 +0100
    19.3 @@ -1,4 +1,4 @@
    19.4 -(*  Title:      HOL/Induct/QuoDataType
    19.5 +(*  Title:      HOL/Induct/QuoDataType.thy
    19.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.7      Copyright   2004  University of Cambridge
    19.8  *)
    20.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Sun Mar 13 22:24:10 2011 +0100
    20.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Sun Mar 13 22:55:50 2011 +0100
    20.3 @@ -1,4 +1,4 @@
    20.4 -(*  Title:      HOL/Induct/QuoNestedDataType
    20.5 +(*  Title:      HOL/Induct/QuoNestedDataType.thy
    20.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    20.7      Copyright   2004  University of Cambridge
    20.8  *)
    21.1 --- a/src/HOL/Int.thy	Sun Mar 13 22:24:10 2011 +0100
    21.2 +++ b/src/HOL/Int.thy	Sun Mar 13 22:55:50 2011 +0100
    21.3 @@ -1,8 +1,6 @@
    21.4 -(*  Title:      Int.thy
    21.5 +(*  Title:      HOL/Int.thy
    21.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    21.7 -                Tobias Nipkow, Florian Haftmann, TU Muenchen
    21.8 -    Copyright   1994  University of Cambridge
    21.9 -
   21.10 +    Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
   21.11  *)
   21.12  
   21.13  header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
    22.1 --- a/src/HOL/Library/Bit.thy	Sun Mar 13 22:24:10 2011 +0100
    22.2 +++ b/src/HOL/Library/Bit.thy	Sun Mar 13 22:55:50 2011 +0100
    22.3 @@ -1,5 +1,5 @@
    22.4 -(* Title:      Bit.thy
    22.5 -   Author:     Brian Huffman
    22.6 +(*  Title:      HOL/Library/Bit.thy
    22.7 +    Author:     Brian Huffman
    22.8  *)
    22.9  
   22.10  header {* The Field of Integers mod 2 *}
    23.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sun Mar 13 22:24:10 2011 +0100
    23.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Mar 13 22:55:50 2011 +0100
    23.3 @@ -1,4 +1,4 @@
    23.4 -(*  Title:      Formal_Power_Series.thy
    23.5 +(*  Title:      HOL/Library/Formal_Power_Series.thy
    23.6      Author:     Amine Chaieb, University of Cambridge
    23.7  *)
    23.8  
    24.1 --- a/src/HOL/Library/Inner_Product.thy	Sun Mar 13 22:24:10 2011 +0100
    24.2 +++ b/src/HOL/Library/Inner_Product.thy	Sun Mar 13 22:55:50 2011 +0100
    24.3 @@ -1,5 +1,5 @@
    24.4 -(* Title:      Inner_Product.thy
    24.5 -   Author:     Brian Huffman
    24.6 +(*  Title:      HOL/Library/Inner_Product.thy
    24.7 +    Author:     Brian Huffman
    24.8  *)
    24.9  
   24.10  header {* Inner Product Spaces and the Gradient Derivative *}
    25.1 --- a/src/HOL/Library/Nat_Bijection.thy	Sun Mar 13 22:24:10 2011 +0100
    25.2 +++ b/src/HOL/Library/Nat_Bijection.thy	Sun Mar 13 22:55:50 2011 +0100
    25.3 @@ -1,4 +1,4 @@
    25.4 -(*  Title:      HOL/Nat_Bijection.thy
    25.5 +(*  Title:      HOL/Library/Nat_Bijection.thy
    25.6      Author:     Brian Huffman
    25.7      Author:     Florian Haftmann
    25.8      Author:     Stefan Richter
    26.1 --- a/src/HOL/Library/Permutations.thy	Sun Mar 13 22:24:10 2011 +0100
    26.2 +++ b/src/HOL/Library/Permutations.thy	Sun Mar 13 22:55:50 2011 +0100
    26.3 @@ -1,5 +1,5 @@
    26.4 -(* Title:      Library/Permutations
    26.5 -   Author:     Amine Chaieb, University of Cambridge
    26.6 +(*  Title:      HOL/Library/Permutations.thy
    26.7 +    Author:     Amine Chaieb, University of Cambridge
    26.8  *)
    26.9  
   26.10  header {* Permutations, both general and specifically on finite sets.*}
    27.1 --- a/src/HOL/Library/Poly_Deriv.thy	Sun Mar 13 22:24:10 2011 +0100
    27.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Sun Mar 13 22:55:50 2011 +0100
    27.3 @@ -1,6 +1,6 @@
    27.4 -(*  Title:      Poly_Deriv.thy
    27.5 +(*  Title:      HOL/Library/Poly_Deriv.thy
    27.6      Author:     Amine Chaieb
    27.7 -                Ported to new Polynomial library by Brian Huffman
    27.8 +    Author:     Brian Huffman
    27.9  *)
   27.10  
   27.11  header{* Polynomials and Differentiation *}
    28.1 --- a/src/HOL/Library/Polynomial.thy	Sun Mar 13 22:24:10 2011 +0100
    28.2 +++ b/src/HOL/Library/Polynomial.thy	Sun Mar 13 22:55:50 2011 +0100
    28.3 @@ -1,6 +1,6 @@
    28.4 -(*  Title:      HOL/Polynomial.thy
    28.5 +(*  Title:      HOL/Library/Polynomial.thy
    28.6      Author:     Brian Huffman
    28.7 -                Based on an earlier development by Clemens Ballarin
    28.8 +    Author:     Clemens Ballarin
    28.9  *)
   28.10  
   28.11  header {* Univariate Polynomials *}
    29.1 --- a/src/HOL/Library/RBT_Impl.thy	Sun Mar 13 22:24:10 2011 +0100
    29.2 +++ b/src/HOL/Library/RBT_Impl.thy	Sun Mar 13 22:55:50 2011 +0100
    29.3 @@ -1,4 +1,4 @@
    29.4 -(*  Title:      RBT_Impl.thy
    29.5 +(*  Title:      HOL/Library/RBT_Impl.thy
    29.6      Author:     Markus Reiter, TU Muenchen
    29.7      Author:     Alexander Krauss, TU Muenchen
    29.8  *)
    30.1 --- a/src/HOL/Ln.thy	Sun Mar 13 22:24:10 2011 +0100
    30.2 +++ b/src/HOL/Ln.thy	Sun Mar 13 22:55:50 2011 +0100
    30.3 @@ -1,4 +1,4 @@
    30.4 -(*  Title:      Ln.thy
    30.5 +(*  Title:      HOL/Ln.thy
    30.6      Author:     Jeremy Avigad
    30.7  *)
    30.8  
    31.1 --- a/src/HOL/Matrix/ComputeFloat.thy	Sun Mar 13 22:24:10 2011 +0100
    31.2 +++ b/src/HOL/Matrix/ComputeFloat.thy	Sun Mar 13 22:55:50 2011 +0100
    31.3 @@ -1,5 +1,5 @@
    31.4 -(*  Title:  HOL/Tools/ComputeFloat.thy
    31.5 -    Author: Steven Obua
    31.6 +(*  Title:      HOL/Matrix/ComputeFloat.thy
    31.7 +    Author:     Steven Obua
    31.8  *)
    31.9  
   31.10  header {* Floating Point Representation of the Reals *}
    32.1 --- a/src/HOL/Matrix/Compute_Oracle/Compute_Oracle.thy	Sun Mar 13 22:24:10 2011 +0100
    32.2 +++ b/src/HOL/Matrix/Compute_Oracle/Compute_Oracle.thy	Sun Mar 13 22:55:50 2011 +0100
    32.3 @@ -1,4 +1,4 @@
    32.4 -(*  Title:      Tools/Compute_Oracle/Compute_Oracle.thy
    32.5 +(*  Title:      HOL/Matrix/Compute_Oracle/Compute_Oracle.thy
    32.6      Author:     Steven Obua, TU Munich
    32.7  
    32.8  Steven Obua's evaluator.
    33.1 --- a/src/HOL/Matrix/Compute_Oracle/am_compiler.ML	Sun Mar 13 22:24:10 2011 +0100
    33.2 +++ b/src/HOL/Matrix/Compute_Oracle/am_compiler.ML	Sun Mar 13 22:55:50 2011 +0100
    33.3 @@ -1,4 +1,4 @@
    33.4 -(*  Title:      Tools/Compute_Oracle/am_compiler.ML
    33.5 +(*  Title:      HOL/Matrix/Compute_Oracle/am_compiler.ML
    33.6      Author:     Steven Obua
    33.7  *)
    33.8  
    34.1 --- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sun Mar 13 22:24:10 2011 +0100
    34.2 +++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sun Mar 13 22:55:50 2011 +0100
    34.3 @@ -1,4 +1,4 @@
    34.4 -(*  Title:      Tools/Compute_Oracle/am_ghc.ML
    34.5 +(*  Title:      HOL/Matrix/Compute_Oracle/am_ghc.ML
    34.6      Author:     Steven Obua
    34.7  *)
    34.8  
    35.1 --- a/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML	Sun Mar 13 22:24:10 2011 +0100
    35.2 +++ b/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML	Sun Mar 13 22:55:50 2011 +0100
    35.3 @@ -1,4 +1,4 @@
    35.4 -(*  Title:      Tools/Compute_Oracle/am_interpreter.ML
    35.5 +(*  Title:      HOL/Matrix/Compute_Oracle/am_interpreter.ML
    35.6      Author:     Steven Obua
    35.7  *)
    35.8  
    36.1 --- a/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Sun Mar 13 22:24:10 2011 +0100
    36.2 +++ b/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Sun Mar 13 22:55:50 2011 +0100
    36.3 @@ -1,4 +1,4 @@
    36.4 -(*  Title:      Tools/Compute_Oracle/am_sml.ML
    36.5 +(*  Title:      HOL/Matrix/Compute_Oracle/am_sml.ML
    36.6      Author:     Steven Obua
    36.7  
    36.8  TODO: "parameterless rewrite cannot be used in pattern": In a lot of
    37.1 --- a/src/HOL/Matrix/Compute_Oracle/compute.ML	Sun Mar 13 22:24:10 2011 +0100
    37.2 +++ b/src/HOL/Matrix/Compute_Oracle/compute.ML	Sun Mar 13 22:55:50 2011 +0100
    37.3 @@ -1,4 +1,4 @@
    37.4 -(*  Title:      Tools/Compute_Oracle/compute.ML
    37.5 +(*  Title:      HOL/Matrix/Compute_Oracle/compute.ML
    37.6      Author:     Steven Obua
    37.7  *)
    37.8  
    38.1 --- a/src/HOL/Matrix/Compute_Oracle/linker.ML	Sun Mar 13 22:24:10 2011 +0100
    38.2 +++ b/src/HOL/Matrix/Compute_Oracle/linker.ML	Sun Mar 13 22:55:50 2011 +0100
    38.3 @@ -1,4 +1,4 @@
    38.4 -(*  Title:      Tools/Compute_Oracle/linker.ML
    38.5 +(*  Title:      HOL/Matrix/Compute_Oracle/linker.ML
    38.6      Author:     Steven Obua
    38.7  
    38.8  This module solves the problem that the computing oracle does not
    39.1 --- a/src/HOL/Matrix/Cplex.thy	Sun Mar 13 22:24:10 2011 +0100
    39.2 +++ b/src/HOL/Matrix/Cplex.thy	Sun Mar 13 22:55:50 2011 +0100
    39.3 @@ -1,4 +1,4 @@
    39.4 -(*  Title:      HOL/Matrix/cplex/Cplex.thy
    39.5 +(*  Title:      HOL/Matrix/Cplex.thy
    39.6      Author:     Steven Obua
    39.7  *)
    39.8  
    40.1 --- a/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML	Sun Mar 13 22:24:10 2011 +0100
    40.2 +++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML	Sun Mar 13 22:55:50 2011 +0100
    40.3 @@ -1,4 +1,4 @@
    40.4 -(*  Title:      sledgehammer_tactics.ML
    40.5 +(*  Title:      HOL/Mirabelle/Tools/sledgehammer_tactics.ML
    40.6      Author:     Jasmin Blanchette, TU Muenchen
    40.7      Copyright   2010
    40.8  
    41.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Mar 13 22:24:10 2011 +0100
    41.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Mar 13 22:55:50 2011 +0100
    41.3 @@ -1,4 +1,4 @@
    41.4 -(*  Title:      HOL/Library/Convex_Euclidean_Space.thy
    41.5 +(*  Title:      HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
    41.6      Author:     Robert Himmelmann, TU Muenchen
    41.7      Author:     Bogdan Grechuk, University of Edinburgh
    41.8  *)
    42.1 --- a/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Mar 13 22:24:10 2011 +0100
    42.2 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Mar 13 22:55:50 2011 +0100
    42.3 @@ -1,5 +1,5 @@
    42.4 -(* Title:      Determinants
    42.5 -   Author:     Amine Chaieb, University of Cambridge
    42.6 +(*  Title:      HOL/Multivariate_Analysis/Determinants.thy
    42.7 +    Author:     Amine Chaieb, University of Cambridge
    42.8  *)
    42.9  
   42.10  header {* Traces, Determinant of square matrices and some properties *}
    43.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Mar 13 22:24:10 2011 +0100
    43.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Mar 13 22:55:50 2011 +0100
    43.3 @@ -1,4 +1,4 @@
    43.4 -(*  Title:      Library/Multivariate_Analysis/Euclidean_Space.thy
    43.5 +(*  Title:      HOL/Multivariate_Analysis/Euclidean_Space.thy
    43.6      Author:     Amine Chaieb, University of Cambridge
    43.7  *)
    43.8  
    44.1 --- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Sun Mar 13 22:24:10 2011 +0100
    44.2 +++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Sun Mar 13 22:55:50 2011 +0100
    44.3 @@ -1,4 +1,4 @@
    44.4 -(*  Title:      Multivariate_Analysis/L2_Norm.thy
    44.5 +(*  Title:      HOL/Multivariate_Analysis/L2_Norm.thy
    44.6      Author:     Brian Huffman, Portland State University
    44.7  *)
    44.8  
    45.1 --- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Sun Mar 13 22:24:10 2011 +0100
    45.2 +++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Sun Mar 13 22:55:50 2011 +0100
    45.3 @@ -1,4 +1,4 @@
    45.4 -(*  Title:      Library/Operator_Norm.thy
    45.5 +(*  Title:      HOL/Multivariate_Analysis/Operator_Norm.thy
    45.6      Author:     Amine Chaieb, University of Cambridge
    45.7  *)
    45.8  
    46.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sun Mar 13 22:24:10 2011 +0100
    46.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sun Mar 13 22:55:50 2011 +0100
    46.3 @@ -1,4 +1,4 @@
    46.4 -(*  Title:      Multivariate_Analysis/Path_Connected.thy
    46.5 +(*  Title:      HOL/Multivariate_Analysis/Path_Connected.thy
    46.6      Author:     Robert Himmelmann, TU Muenchen
    46.7  *)
    46.8  
    47.1 --- a/src/HOL/NSA/Filter.thy	Sun Mar 13 22:24:10 2011 +0100
    47.2 +++ b/src/HOL/NSA/Filter.thy	Sun Mar 13 22:55:50 2011 +0100
    47.3 @@ -1,4 +1,4 @@
    47.4 -(*  Title:      Filter.thy
    47.5 +(*  Title:      HOL/NSA/Filter.thy
    47.6      Author:     Jacques D. Fleuriot, University of Cambridge
    47.7      Author:     Lawrence C Paulson
    47.8      Author:     Brian Huffman
    48.1 --- a/src/HOL/NSA/HLim.thy	Sun Mar 13 22:24:10 2011 +0100
    48.2 +++ b/src/HOL/NSA/HLim.thy	Sun Mar 13 22:55:50 2011 +0100
    48.3 @@ -1,4 +1,4 @@
    48.4 -(*  Title:      HLim.thy
    48.5 +(*  Title:      HOL/NSA/HLim.thy
    48.6      Author:     Jacques D. Fleuriot, University of Cambridge
    48.7      Author:     Lawrence C Paulson
    48.8  *)
    49.1 --- a/src/HOL/NSA/NSComplex.thy	Sun Mar 13 22:24:10 2011 +0100
    49.2 +++ b/src/HOL/NSA/NSComplex.thy	Sun Mar 13 22:55:50 2011 +0100
    49.3 @@ -1,7 +1,6 @@
    49.4 -(*  Title:       NSComplex.thy
    49.5 -    Author:      Jacques D. Fleuriot
    49.6 -    Copyright:   2001  University of Edinburgh
    49.7 -    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
    49.8 +(*  Title:      HOL/NSA/NSComplex.thy
    49.9 +    Author:     Jacques D. Fleuriot, University of Edinburgh
   49.10 +    Author:     Lawrence C Paulson
   49.11  *)
   49.12  
   49.13  header{*Nonstandard Complex Numbers*}
    50.1 --- a/src/HOL/Number_Theory/Binomial.thy	Sun Mar 13 22:24:10 2011 +0100
    50.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Sun Mar 13 22:55:50 2011 +0100
    50.3 @@ -1,4 +1,4 @@
    50.4 -(*  Title:      Binomial.thy
    50.5 +(*  Title:      HOL/Number_Theory/Binomial.thy
    50.6      Authors:    Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
    50.7  
    50.8  Defines the "choose" function, and establishes basic properties.
    51.1 --- a/src/HOL/Number_Theory/Cong.thy	Sun Mar 13 22:24:10 2011 +0100
    51.2 +++ b/src/HOL/Number_Theory/Cong.thy	Sun Mar 13 22:55:50 2011 +0100
    51.3 @@ -1,4 +1,4 @@
    51.4 -(*  Title:      HOL/Library/Cong.thy
    51.5 +(*  Title:      HOL/Number_Theory/Cong.thy
    51.6      Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
    51.7                  Thomas M. Rasmussen, Jeremy Avigad
    51.8  
    52.1 --- a/src/HOL/Number_Theory/Fib.thy	Sun Mar 13 22:24:10 2011 +0100
    52.2 +++ b/src/HOL/Number_Theory/Fib.thy	Sun Mar 13 22:55:50 2011 +0100
    52.3 @@ -1,5 +1,6 @@
    52.4 -(*  Title:      Fib.thy
    52.5 -    Authors:    Lawrence C. Paulson, Jeremy Avigad
    52.6 +(*  Title:      HOL/Number_Theory/Fib.thy
    52.7 +    Author:     Lawrence C. Paulson
    52.8 +    Author:     Jeremy Avigad
    52.9  
   52.10  Defines the fibonacci function.
   52.11  
    53.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Sun Mar 13 22:24:10 2011 +0100
    53.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Sun Mar 13 22:55:50 2011 +0100
    53.3 @@ -1,4 +1,4 @@
    53.4 -(*  Title:      MiscAlgebra.thy
    53.5 +(*  Title:      HOL/Number_Theory/MiscAlgebra.thy
    53.6      Author:     Jeremy Avigad
    53.7  
    53.8  These are things that can be added to the Algebra library.
    54.1 --- a/src/HOL/Number_Theory/Residues.thy	Sun Mar 13 22:24:10 2011 +0100
    54.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sun Mar 13 22:55:50 2011 +0100
    54.3 @@ -1,8 +1,8 @@
    54.4 -(*  Title:      HOL/Library/Residues.thy
    54.5 +(*  Title:      HOL/Number_Theory/Residues.thy
    54.6      Author:     Jeremy Avigad
    54.7  
    54.8  An algebraic treatment of residue rings, and resulting proofs of
    54.9 -Euler's theorem and Wilson's theorem. 
   54.10 +Euler's theorem and Wilson's theorem.
   54.11  *)
   54.12  
   54.13  header {* Residue rings *}
    55.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Sun Mar 13 22:24:10 2011 +0100
    55.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Sun Mar 13 22:55:50 2011 +0100
    55.3 @@ -1,4 +1,4 @@
    55.4 -(*  Title:      UniqueFactorization.thy
    55.5 +(*  Title:      HOL/Number_Theory/UniqueFactorization.thy
    55.6      Author:     Jeremy Avigad
    55.7  
    55.8  Unique factorization for the natural numbers and the integers.
    56.1 --- a/src/HOL/Parity.thy	Sun Mar 13 22:24:10 2011 +0100
    56.2 +++ b/src/HOL/Parity.thy	Sun Mar 13 22:55:50 2011 +0100
    56.3 @@ -1,5 +1,6 @@
    56.4 -(*  Title:      HOL/Library/Parity.thy
    56.5 -    Author:     Jeremy Avigad, Jacques D. Fleuriot
    56.6 +(*  Title:      HOL/Parity.thy
    56.7 +    Author:     Jeremy Avigad
    56.8 +    Author:     Jacques D. Fleuriot
    56.9  *)
   56.10  
   56.11  header {* Even and Odd for int and nat *}
    57.1 --- a/src/HOL/Probability/Complete_Measure.thy	Sun Mar 13 22:24:10 2011 +0100
    57.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Sun Mar 13 22:55:50 2011 +0100
    57.3 @@ -1,6 +1,7 @@
    57.4 -(*  Title:      Complete_Measure.thy
    57.5 +(*  Title:      HOL/Probability/Complete_Measure.thy
    57.6      Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
    57.7  *)
    57.8 +
    57.9  theory Complete_Measure
   57.10  imports Product_Measure
   57.11  begin
    58.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Sun Mar 13 22:24:10 2011 +0100
    58.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Sun Mar 13 22:55:50 2011 +0100
    58.3 @@ -1,7 +1,7 @@
    58.4 -(*  Title:      Sigma_Algebra.thy
    58.5 -    Author:     Stefan Richter, Markus Wenzel, TU Muenchen
    58.6 -    Plus material from the Hurd/Coble measure theory development,
    58.7 -    translated by Lawrence Paulson.
    58.8 +(*  Title:      HOL/Probability/Sigma_Algebra.thy
    58.9 +    Author:     Stefan Richter
   58.10 +    Author:     Markus Wenzel
   58.11 +    Author:     Lawrence Paulson
   58.12  *)
   58.13  
   58.14  header {* Sigma Algebras *}
    59.1 --- a/src/HOL/Quotient.thy	Sun Mar 13 22:24:10 2011 +0100
    59.2 +++ b/src/HOL/Quotient.thy	Sun Mar 13 22:55:50 2011 +0100
    59.3 @@ -1,4 +1,4 @@
    59.4 -(*  Title:      Quotient.thy
    59.5 +(*  Title:      HOL/Quotient.thy
    59.6      Author:     Cezary Kaliszyk and Christian Urban
    59.7  *)
    59.8  
    60.1 --- a/src/HOL/Statespace/StateFun.thy	Sun Mar 13 22:24:10 2011 +0100
    60.2 +++ b/src/HOL/Statespace/StateFun.thy	Sun Mar 13 22:55:50 2011 +0100
    60.3 @@ -1,4 +1,4 @@
    60.4 -(*  Title:      StateFun.thy
    60.5 +(*  Title:      HOL/Statespace/StateFun.thy
    60.6      Author:     Norbert Schirmer, TU Muenchen
    60.7  *)
    60.8  
    61.1 --- a/src/HOL/Statespace/StateSpaceEx.thy	Sun Mar 13 22:24:10 2011 +0100
    61.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Sun Mar 13 22:55:50 2011 +0100
    61.3 @@ -1,4 +1,4 @@
    61.4 -(*  Title:      StateSpaceEx.thy
    61.5 +(*  Title:      HOL/Statespace/StateSpaceEx.thy
    61.6      Author:     Norbert Schirmer, TU Muenchen
    61.7  *)
    61.8  
    62.1 --- a/src/HOL/Statespace/StateSpaceLocale.thy	Sun Mar 13 22:24:10 2011 +0100
    62.2 +++ b/src/HOL/Statespace/StateSpaceLocale.thy	Sun Mar 13 22:55:50 2011 +0100
    62.3 @@ -1,4 +1,4 @@
    62.4 -(*  Title:      StateSpaceLocale.thy
    62.5 +(*  Title:      HOL/Statespace/StateSpaceLocale.thy
    62.6      Author:     Norbert Schirmer, TU Muenchen
    62.7  *)
    62.8  
    63.1 --- a/src/HOL/Statespace/StateSpaceSyntax.thy	Sun Mar 13 22:24:10 2011 +0100
    63.2 +++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Sun Mar 13 22:55:50 2011 +0100
    63.3 @@ -1,4 +1,4 @@
    63.4 -(*  Title:      StateSpaceSyntax.thy
    63.5 +(*  Title:      HOL/Statespace/StateSpaceSyntax.thy
    63.6      Author:     Norbert Schirmer, TU Muenchen
    63.7  *)
    63.8  
    64.1 --- a/src/HOL/Word/Tools/smt_word.ML	Sun Mar 13 22:24:10 2011 +0100
    64.2 +++ b/src/HOL/Word/Tools/smt_word.ML	Sun Mar 13 22:55:50 2011 +0100
    64.3 @@ -1,4 +1,4 @@
    64.4 -(*  Title:      HOL/Tools/SMT/smt_word.ML
    64.5 +(*  Title:      HOL/Word/Tools/smt_word.ML
    64.6      Author:     Sascha Boehme, TU Muenchen
    64.7  
    64.8  SMT setup for words.
    65.1 --- a/src/HOL/ex/Arithmetic_Series_Complex.thy	Sun Mar 13 22:24:10 2011 +0100
    65.2 +++ b/src/HOL/ex/Arithmetic_Series_Complex.thy	Sun Mar 13 22:55:50 2011 +0100
    65.3 @@ -1,4 +1,4 @@
    65.4 -(*  Title:      HOL/ex/Arithmetic_Series_Complex
    65.5 +(*  Title:      HOL/ex/Arithmetic_Series_Complex.thy
    65.6      Author:     Benjamin Porter, 2006
    65.7  *)
    65.8  
    66.1 --- a/src/HOL/ex/Classical.thy	Sun Mar 13 22:24:10 2011 +0100
    66.2 +++ b/src/HOL/ex/Classical.thy	Sun Mar 13 22:55:50 2011 +0100
    66.3 @@ -1,4 +1,4 @@
    66.4 -(*  Title:      HOL/ex/Classical
    66.5 +(*  Title:      HOL/ex/Classical.thy
    66.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    66.7      Copyright   1994  University of Cambridge
    66.8  *)
    67.1 --- a/src/HOL/ex/CodegenSML_Test.thy	Sun Mar 13 22:24:10 2011 +0100
    67.2 +++ b/src/HOL/ex/CodegenSML_Test.thy	Sun Mar 13 22:55:50 2011 +0100
    67.3 @@ -1,5 +1,7 @@
    67.4 -(*  Title:      Test file for Stefan Berghofer's SML code generator
    67.5 +(*  Title:      HOL/ex/CodegenSML_Test.thy
    67.6      Author:     Tobias Nipkow, TU Muenchen
    67.7 +
    67.8 +Test file for Stefan Berghofer's SML code generator.
    67.9  *)
   67.10  
   67.11  theory CodegenSML_Test
    68.1 --- a/src/HOL/ex/Sorting.thy	Sun Mar 13 22:24:10 2011 +0100
    68.2 +++ b/src/HOL/ex/Sorting.thy	Sun Mar 13 22:55:50 2011 +0100
    68.3 @@ -1,4 +1,4 @@
    68.4 -(*  Title:      HOL/ex/sorting.thy
    68.5 +(*  Title:      HOL/ex/Sorting.thy
    68.6      Author:     Tobias Nipkow
    68.7      Copyright   1994 TU Muenchen
    68.8  *)
    69.1 --- a/src/HOL/ex/While_Combinator_Example.thy	Sun Mar 13 22:24:10 2011 +0100
    69.2 +++ b/src/HOL/ex/While_Combinator_Example.thy	Sun Mar 13 22:55:50 2011 +0100
    69.3 @@ -1,4 +1,4 @@
    69.4 -(*  Title:      HOL/Library/While_Combinator.thy
    69.5 +(*  Title:      HOL/ex/While_Combinator_Example.thy
    69.6      Author:     Tobias Nipkow
    69.7      Copyright   2000 TU Muenchen
    69.8  *)
    70.1 --- a/src/Pure/Isar/generic_target.ML	Sun Mar 13 22:24:10 2011 +0100
    70.2 +++ b/src/Pure/Isar/generic_target.ML	Sun Mar 13 22:55:50 2011 +0100
    70.3 @@ -1,4 +1,4 @@
    70.4 -(*  Title:      Pure/Isar/theory_target.ML
    70.5 +(*  Title:      Pure/Isar/generic_target.ML
    70.6      Author:     Makarius
    70.7      Author:     Florian Haftmann, TU Muenchen
    70.8  
    71.1 --- a/src/Pure/Isar/named_target.ML	Sun Mar 13 22:24:10 2011 +0100
    71.2 +++ b/src/Pure/Isar/named_target.ML	Sun Mar 13 22:55:50 2011 +0100
    71.3 @@ -1,4 +1,4 @@
    71.4 -(*  Title:      Pure/Isar/theory_target.ML
    71.5 +(*  Title:      Pure/Isar/named_target.ML
    71.6      Author:     Makarius
    71.7      Author:     Florian Haftmann, TU Muenchen
    71.8  
    72.1 --- a/src/Sequents/LK.thy	Sun Mar 13 22:24:10 2011 +0100
    72.2 +++ b/src/Sequents/LK.thy	Sun Mar 13 22:55:50 2011 +0100
    72.3 @@ -1,4 +1,4 @@
    72.4 -(*  Title:      LK/LK.ML
    72.5 +(*  Title:      Sequents/LK.thy
    72.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    72.7      Copyright   1993  University of Cambridge
    72.8  
    73.1 --- a/src/Sequents/LK/Hard_Quantifiers.thy	Sun Mar 13 22:24:10 2011 +0100
    73.2 +++ b/src/Sequents/LK/Hard_Quantifiers.thy	Sun Mar 13 22:55:50 2011 +0100
    73.3 @@ -1,4 +1,4 @@
    73.4 -(*  Title:      LK/Hard_Quantifiers.thy
    73.5 +(*  Title:      Sequents/LK/Hard_Quantifiers.thy
    73.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    73.7      Copyright   1992  University of Cambridge
    73.8  
    74.1 --- a/src/Sequents/LK/Propositional.thy	Sun Mar 13 22:24:10 2011 +0100
    74.2 +++ b/src/Sequents/LK/Propositional.thy	Sun Mar 13 22:55:50 2011 +0100
    74.3 @@ -1,4 +1,4 @@
    74.4 -(*  Title:      LK/Propositional.thy
    74.5 +(*  Title:      Sequents/LK/Propositional.thy
    74.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    74.7      Copyright   1992  University of Cambridge
    74.8  *)
    75.1 --- a/src/Sequents/LK/Quantifiers.thy	Sun Mar 13 22:24:10 2011 +0100
    75.2 +++ b/src/Sequents/LK/Quantifiers.thy	Sun Mar 13 22:55:50 2011 +0100
    75.3 @@ -1,4 +1,4 @@
    75.4 -(*  Title:      LK/Quantifiers.thy
    75.5 +(*  Title:      Sequents/LK/Quantifiers.thy
    75.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    75.7      Copyright   1992  University of Cambridge
    75.8  
    76.1 --- a/src/Sequents/LK0.thy	Sun Mar 13 22:24:10 2011 +0100
    76.2 +++ b/src/Sequents/LK0.thy	Sun Mar 13 22:55:50 2011 +0100
    76.3 @@ -1,4 +1,4 @@
    76.4 -(*  Title:      LK/LK0.thy
    76.5 +(*  Title:      Sequents/LK0.thy
    76.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    76.7      Copyright   1993  University of Cambridge
    76.8  
    77.1 --- a/src/Sequents/S43.thy	Sun Mar 13 22:24:10 2011 +0100
    77.2 +++ b/src/Sequents/S43.thy	Sun Mar 13 22:55:50 2011 +0100
    77.3 @@ -1,4 +1,4 @@
    77.4 -(*  Title:      Modal/S43.thy
    77.5 +(*  Title:      Sequents/S43.thy
    77.6      Author:     Martin Coen
    77.7      Copyright   1991  University of Cambridge
    77.8