fixed title
authorhaftmann
Sat Sep 15 19:27:35 2007 +0200 (2007-09-15)
changeset 2458401e83ffa6c54
parent 24583 d77e4d48e497
child 24585 c359896d0f48
fixed title
Admin/de_overload.ML
doc-src/AxClass/Nat/NatClass.ML
doc-src/antiquote_setup.ML
src/FOLP/FOLP_lemmas.ML
src/FOLP/ex/Nat.ML
src/FOLP/ex/Prolog.ML
src/FOLP/intprover.ML
src/HOL/Hoare/ROOT.ML
src/HOL/Import/xml.ML
src/HOL/Matrix/cplex/matrixlp.ML
src/HOL/Nominal/ROOT.ML
src/HOL/Real/float_arith.ML
src/HOL/TLA/ROOT.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/cooper_data.ML
src/HOL/Tools/Qelim/ferrante_rackoff.ML
src/HOL/Tools/Qelim/ferrante_rackoff_data.ML
src/HOL/Tools/Qelim/generated_cooper.ML
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/function_package/pattern_split.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/split_rule.ML
src/HOL/Tools/watcher.ML
src/HOL/ex/svc_funcs.ML
src/HOLCF/IOA/ABP/ROOT.ML
src/HOLCF/IOA/NTP/ROOT.ML
src/HOLCF/IOA/ROOT.ML
src/HOLCF/IOA/Storage/ROOT.ML
src/HOLCF/IOA/ex/ROOT.ML
src/Provers/Arith/abel_cancel.ML
src/Pure/General/xml.ML
src/Pure/ML-Systems/overloading_smlnj.ML
src/Pure/ML-Systems/polyml-5.1.ML
src/Pure/ProofGeneral/pgml.ML
src/Pure/Thy/html.ML
src/Sequents/LK/ROOT.ML
src/Sequents/modal.ML
src/Tools/Compute_Oracle/am_compiler.ML
src/Tools/Compute_Oracle/am_ghc.ML
src/Tools/Compute_Oracle/am_interpreter.ML
src/Tools/Compute_Oracle/am_sml.ML
src/Tools/Compute_Oracle/compute.ML
src/Tools/Compute_Oracle/linker.ML
src/Tools/float.ML
src/Tools/integer.ML
src/Tools/rat.ML
src/ZF/Coind/ROOT.ML
src/ZF/Tools/cartprod.ML
src/ZF/Tools/twos_compl.ML
     1.1 --- a/Admin/de_overload.ML	Sat Sep 15 19:26:28 2007 +0200
     1.2 +++ b/Admin/de_overload.ML	Sat Sep 15 19:27:35 2007 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      Pure/ML-Systems/de_overload.ML
     1.5 +(*  Title:      Admin/de_overload.ML
     1.6      ID:         $Id$
     1.7      Author:     Makarius
     1.8  
     2.1 --- a/doc-src/AxClass/Nat/NatClass.ML	Sat Sep 15 19:26:28 2007 +0200
     2.2 +++ b/doc-src/AxClass/Nat/NatClass.ML	Sat Sep 15 19:27:35 2007 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      FOL/ex/NatClass.ML
     2.5 +(*  Title:      Doc/AxClass/Nat/NatClass.ML
     2.6      ID:         $Id$
     2.7      Author:     Markus Wenzel, TU Muenchen
     2.8  
     3.1 --- a/doc-src/antiquote_setup.ML	Sat Sep 15 19:26:28 2007 +0200
     3.2 +++ b/doc-src/antiquote_setup.ML	Sat Sep 15 19:27:35 2007 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      antiquote_setup.ML
     3.5 +(*  Title:      Doc/antiquote_setup.ML
     3.6      ID:         $Id$
     3.7      Author:     Makarius
     3.8  
     4.1 --- a/src/FOLP/FOLP_lemmas.ML	Sat Sep 15 19:26:28 2007 +0200
     4.2 +++ b/src/FOLP/FOLP_lemmas.ML	Sat Sep 15 19:27:35 2007 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      FOLP/FOLP.ML
     4.5 +(*  Title:      FOLP/FOLP_lemmas.ML
     4.6      ID:         $Id$
     4.7      Author:     Martin D Coen, Cambridge University Computer Laboratory
     4.8      Copyright   1991  University of Cambridge
     5.1 --- a/src/FOLP/ex/Nat.ML	Sat Sep 15 19:26:28 2007 +0200
     5.2 +++ b/src/FOLP/ex/Nat.ML	Sat Sep 15 19:27:35 2007 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      FOLP/ex/nat.ML
     5.5 +(*  Title:      FOLP/ex/Nat.ML
     5.6      ID:         $Id$
     5.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.8      Copyright   1992  University of Cambridge
     6.1 --- a/src/FOLP/ex/Prolog.ML	Sat Sep 15 19:26:28 2007 +0200
     6.2 +++ b/src/FOLP/ex/Prolog.ML	Sat Sep 15 19:27:35 2007 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      FOLP/ex/prolog.ML
     6.5 +(*  Title:      FOLP/ex/Prolog.ML
     6.6      ID:         $Id$
     6.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.8      Copyright   1992  University of Cambridge
     7.1 --- a/src/FOLP/intprover.ML	Sat Sep 15 19:26:28 2007 +0200
     7.2 +++ b/src/FOLP/intprover.ML	Sat Sep 15 19:27:35 2007 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      FOLP/int-prover.ML
     7.5 +(*  Title:      FOLP/intprover.ML
     7.6      ID:         $Id$
     7.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.8      Copyright   1992  University of Cambridge
     8.1 --- a/src/HOL/Hoare/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
     8.2 +++ b/src/HOL/Hoare/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOL/IMP/ROOT.ML
     8.5 +(*  Title:      HOL/Hoare/ROOT.ML
     8.6      ID:         $Id$
     8.7      Author:     Tobias Nipkow
     8.8      Copyright   1998-2003 TUM
     9.1 --- a/src/HOL/Import/xml.ML	Sat Sep 15 19:26:28 2007 +0200
     9.2 +++ b/src/HOL/Import/xml.ML	Sat Sep 15 19:27:35 2007 +0200
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      Pure/General/xml.ML
     9.5 +(*  Title:      HOL/Import/xml.ML
     9.6      ID:         $Id$
     9.7      Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
     9.8  
    10.1 --- a/src/HOL/Matrix/cplex/matrixlp.ML	Sat Sep 15 19:26:28 2007 +0200
    10.2 +++ b/src/HOL/Matrix/cplex/matrixlp.ML	Sat Sep 15 19:27:35 2007 +0200
    10.3 @@ -1,4 +1,4 @@
    10.4 -(*  Title:      HOL/Matrix/cplex/MatrixLP.ML
    10.5 +(*  Title:      HOL/Matrix/cplex/matrixlp.ML
    10.6      ID:         $Id$
    10.7      Author:     Steven Obua
    10.8  *)
    11.1 --- a/src/HOL/Nominal/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
    11.2 +++ b/src/HOL/Nominal/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
    11.3 @@ -1,4 +1,4 @@
    11.4 -(*  Title:      HOL/Nominal/nominal_atoms.ML
    11.5 +(*  Title:      HOL/Nominal/ROOT.ML
    11.6      ID:         $Id$
    11.7      Author:     Stefan Berghofer and Christian Urban, TU Muenchen
    11.8  
    12.1 --- a/src/HOL/Real/float_arith.ML	Sat Sep 15 19:26:28 2007 +0200
    12.2 +++ b/src/HOL/Real/float_arith.ML	Sat Sep 15 19:27:35 2007 +0200
    12.3 @@ -1,5 +1,5 @@
    12.4 -(*  Title: HOL/Real/Float.ML
    12.5 -    ID:    $Id$
    12.6 +(*  Title:  HOL/Real/float_arith.ML
    12.7 +    ID:     $Id$
    12.8      Author: Steven Obua
    12.9  *)
   12.10  
    13.1 --- a/src/HOL/TLA/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
    13.2 +++ b/src/HOL/TLA/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
    13.3 @@ -1,4 +1,4 @@
    13.4 -(*  Title:      TLA/ROOT.ML
    13.5 +(*  Title:      HOL/TLA/ROOT.ML
    13.6      ID:         $Id$
    13.7  
    13.8  Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
    14.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Sep 15 19:26:28 2007 +0200
    14.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Sep 15 19:27:35 2007 +0200
    14.3 @@ -1,4 +1,4 @@
    14.4 -(*  Title:      HOL/Tools/Presburger/cooper.ML
    14.5 +(*  Title:      HOL/Tools/Qelim/cooper.ML
    14.6      ID:         $Id$
    14.7      Author:     Amine Chaieb, TU Muenchen
    14.8  *)
    15.1 --- a/src/HOL/Tools/Qelim/cooper_data.ML	Sat Sep 15 19:26:28 2007 +0200
    15.2 +++ b/src/HOL/Tools/Qelim/cooper_data.ML	Sat Sep 15 19:27:35 2007 +0200
    15.3 @@ -1,4 +1,4 @@
    15.4 -(*  Title:      HOL/Tools/Presburger/cooper_data.ML
    15.5 +(*  Title:      HOL/Tools/Qelim/cooper_data.ML
    15.6      ID:         $Id$
    15.7      Author:     Amine Chaieb, TU Muenchen
    15.8  *)
    16.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sat Sep 15 19:26:28 2007 +0200
    16.2 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sat Sep 15 19:27:35 2007 +0200
    16.3 @@ -1,4 +1,4 @@
    16.4 -(* Title:      HOL/Tools/ferrante_rackoff.ML
    16.5 +(* Title:      HOL/Tools/Qelim/ferrante_rackoff.ML
    16.6     ID:         $Id$
    16.7     Author:     Amine Chaieb, TU Muenchen
    16.8  
    17.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sat Sep 15 19:26:28 2007 +0200
    17.2 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sat Sep 15 19:27:35 2007 +0200
    17.3 @@ -1,4 +1,4 @@
    17.4 -(* Title:      HOL/Tools/ferrante_rackoff_data.ML
    17.5 +(* Title:      HOL/Tools/Qelim/ferrante_rackoff_data.ML
    17.6     ID:         $Id$
    17.7     Author:     Amine Chaieb, TU Muenchen
    17.8  
    18.1 --- a/src/HOL/Tools/Qelim/generated_cooper.ML	Sat Sep 15 19:26:28 2007 +0200
    18.2 +++ b/src/HOL/Tools/Qelim/generated_cooper.ML	Sat Sep 15 19:27:35 2007 +0200
    18.3 @@ -1,4 +1,4 @@
    18.4 -(*  Title:      HOL/Tools/Presburger/generated_cooper.ML
    18.5 +(*  Title:      HOL/Tools/Qelim/generated_cooper.ML
    18.6      ID:         $Id$
    18.7  
    18.8  This file is generated from HOL/ex/Reflected_Presburger.thy.  DO NOT EDIT.
    19.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Sat Sep 15 19:26:28 2007 +0200
    19.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Sat Sep 15 19:27:35 2007 +0200
    19.3 @@ -1,4 +1,4 @@
    19.4 -(*  Title:      HOL/Tools/Presburger/presburger.ML
    19.5 +(*  Title:      HOL/Tools/Qelim/presburger.ML
    19.6      ID:         $Id$
    19.7      Author:     Amine Chaieb, TU Muenchen
    19.8  *)
    20.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Sat Sep 15 19:26:28 2007 +0200
    20.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Sat Sep 15 19:27:35 2007 +0200
    20.3 @@ -1,4 +1,4 @@
    20.4 -(*  Title:      HOL/Tools/function_package/lib.ML
    20.5 +(*  Title:      HOL/Tools/function_package/fundef_lib.ML
    20.6      ID:         $Id$
    20.7      Author:     Alexander Krauss, TU Muenchen
    20.8  
    21.1 --- a/src/HOL/Tools/function_package/pattern_split.ML	Sat Sep 15 19:26:28 2007 +0200
    21.2 +++ b/src/HOL/Tools/function_package/pattern_split.ML	Sat Sep 15 19:27:35 2007 +0200
    21.3 @@ -1,4 +1,4 @@
    21.4 -(*  Title:      HOL/Tools/function_package/fundef_package.ML
    21.5 +(*  Title:      HOL/Tools/function_package/pattern_split.ML
    21.6      ID:         $Id$
    21.7      Author:     Alexander Krauss, TU Muenchen
    21.8  
    22.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sat Sep 15 19:26:28 2007 +0200
    22.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sat Sep 15 19:27:35 2007 +0200
    22.3 @@ -1,4 +1,4 @@
    22.4 -(*  Title:      HOL/inductive_codegen.ML
    22.5 +(*  Title:      HOL/Tools/inductive_codegen.ML
    22.6      ID:         $Id$
    22.7      Author:     Stefan Berghofer, TU Muenchen
    22.8  
    23.1 --- a/src/HOL/Tools/recfun_codegen.ML	Sat Sep 15 19:26:28 2007 +0200
    23.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Sat Sep 15 19:27:35 2007 +0200
    23.3 @@ -1,4 +1,4 @@
    23.4 -(*  Title:      HOL/recfun_codegen.ML
    23.5 +(*  Title:      HOL/Tools/recfun_codegen.ML
    23.6      ID:         $Id$
    23.7      Author:     Stefan Berghofer, TU Muenchen
    23.8  
    24.1 --- a/src/HOL/Tools/split_rule.ML	Sat Sep 15 19:26:28 2007 +0200
    24.2 +++ b/src/HOL/Tools/split_rule.ML	Sat Sep 15 19:27:35 2007 +0200
    24.3 @@ -1,4 +1,4 @@
    24.4 -(*  Title:      Tools/split_rule.ML
    24.5 +(*  Title:      HOL/Tools/split_rule.ML
    24.6      ID:         $Id$
    24.7      Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
    24.8  
    25.1 --- a/src/HOL/Tools/watcher.ML	Sat Sep 15 19:26:28 2007 +0200
    25.2 +++ b/src/HOL/Tools/watcher.ML	Sat Sep 15 19:27:35 2007 +0200
    25.3 @@ -1,4 +1,4 @@
    25.4 -(*  Title:      Watcher.ML
    25.5 +(*  Title:      HOL/Tools/watcher.ML
    25.6      ID:         $Id$
    25.7      Author:     Claire Quigley
    25.8      Copyright   2004  University of Cambridge
    26.1 --- a/src/HOL/ex/svc_funcs.ML	Sat Sep 15 19:26:28 2007 +0200
    26.2 +++ b/src/HOL/ex/svc_funcs.ML	Sat Sep 15 19:27:35 2007 +0200
    26.3 @@ -1,4 +1,4 @@
    26.4 -(*  Title:      HOL/Tools/svc_funcs.ML
    26.5 +(*  Title:      HOL/ex/svc_funcs.ML
    26.6      ID:         $Id$
    26.7      Author:     Lawrence C Paulson
    26.8      Copyright   1999  University of Cambridge
    27.1 --- a/src/HOLCF/IOA/ABP/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
    27.2 +++ b/src/HOLCF/IOA/ABP/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
    27.3 @@ -1,4 +1,4 @@
    27.4 -(*  Title:      HOL/IOA/ABP/ROOT.ML
    27.5 +(*  Title:      HOLCF/IOA/ABP/ROOT.ML
    27.6      ID:         $Id$
    27.7      Author:     Olaf Mueller
    27.8  
    28.1 --- a/src/HOLCF/IOA/NTP/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
    28.2 +++ b/src/HOLCF/IOA/NTP/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
    28.3 @@ -1,4 +1,4 @@
    28.4 -(*  Title:      HOL/IOA/examples/NTP/ROOT.ML
    28.5 +(*  Title:      HOLCF/IOA/NTP/ROOT.ML
    28.6      ID:         $Id$
    28.7      Author:     Tobias Nipkow & Konrad Slind
    28.8  
    29.1 --- a/src/HOLCF/IOA/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
    29.2 +++ b/src/HOLCF/IOA/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
    29.3 @@ -1,4 +1,4 @@
    29.4 -(*  Title:      HOL/IOA/ROOT.ML
    29.5 +(*  Title:      HOLCF/IOA/ROOT.ML
    29.6      ID:         $Id$
    29.7      Author:     Olaf Mueller
    29.8  
    30.1 --- a/src/HOLCF/IOA/Storage/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
    30.2 +++ b/src/HOLCF/IOA/Storage/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
    30.3 @@ -1,4 +1,4 @@
    30.4 -(*  Title:      HOL/IOA/Storage/ROOT.ML
    30.5 +(*  Title:      HOLCF/IOA/Storage/ROOT.ML
    30.6      ID:         $Id$
    30.7      Author:     Olaf Mueller
    30.8  
    31.1 --- a/src/HOLCF/IOA/ex/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
    31.2 +++ b/src/HOLCF/IOA/ex/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
    31.3 @@ -1,4 +1,4 @@
    31.4 -(*  Title:      HOL/IOA/ex/ROOT.ML
    31.5 +(*  Title:      HOLCF/IOA/ex/ROOT.ML
    31.6      ID:         $Id$
    31.7      Author:     Olaf Mueller
    31.8  *)
    32.1 --- a/src/Provers/Arith/abel_cancel.ML	Sat Sep 15 19:26:28 2007 +0200
    32.2 +++ b/src/Provers/Arith/abel_cancel.ML	Sat Sep 15 19:27:35 2007 +0200
    32.3 @@ -1,4 +1,4 @@
    32.4 -(*  Title:      HOL/OrderedGroup.ML
    32.5 +(*  Title:      Provers/Arith/abel_cancel.ML
    32.6      ID:         $Id$
    32.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    32.8      Copyright   1998  University of Cambridge
    33.1 --- a/src/Pure/General/xml.ML	Sat Sep 15 19:26:28 2007 +0200
    33.2 +++ b/src/Pure/General/xml.ML	Sat Sep 15 19:27:35 2007 +0200
    33.3 @@ -1,4 +1,4 @@
    33.4 -(*  Title:      Pure/Tools/xml.ML
    33.5 +(*  Title:      Pure/General/xml.ML
    33.6      ID:         $Id$
    33.7      Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
    33.8  
    34.1 --- a/src/Pure/ML-Systems/overloading_smlnj.ML	Sat Sep 15 19:26:28 2007 +0200
    34.2 +++ b/src/Pure/ML-Systems/overloading_smlnj.ML	Sat Sep 15 19:27:35 2007 +0200
    34.3 @@ -1,4 +1,4 @@
    34.4 -(*  Title:      Pure/ML-Systems/overloading-smlnj.ML
    34.5 +(*  Title:      Pure/ML-Systems/overloading_smlnj.ML
    34.6      ID:         $Id$
    34.7      Author:     Makarius
    34.8  
    35.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Sat Sep 15 19:26:28 2007 +0200
    35.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Sat Sep 15 19:27:35 2007 +0200
    35.3 @@ -1,4 +1,4 @@
    35.4 -(*  Title:      Pure/ML-Systems/polyml-5.0.ML
    35.5 +(*  Title:      Pure/ML-Systems/polyml-5.1.ML
    35.6      ID:         $Id$
    35.7  
    35.8  Compatibility wrapper for Poly/ML 5.1.
    36.1 --- a/src/Pure/ProofGeneral/pgml.ML	Sat Sep 15 19:26:28 2007 +0200
    36.2 +++ b/src/Pure/ProofGeneral/pgml.ML	Sat Sep 15 19:27:35 2007 +0200
    36.3 @@ -1,4 +1,4 @@
    36.4 -(*  Title:      Pure/ProofGeneral/pgip_types.ML
    36.5 +(*  Title:      Pure/ProofGeneral/pgml.ML
    36.6      ID:         $Id$
    36.7      Author:     David Aspinall
    36.8  
    37.1 --- a/src/Pure/Thy/html.ML	Sat Sep 15 19:26:28 2007 +0200
    37.2 +++ b/src/Pure/Thy/html.ML	Sat Sep 15 19:27:35 2007 +0200
    37.3 @@ -1,4 +1,4 @@
    37.4 -(*  Title:      Pure/Thy/HTML.ML
    37.5 +(*  Title:      Pure/Thy/html.ML
    37.6      ID:         $Id$
    37.7      Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
    37.8  
    38.1 --- a/src/Sequents/LK/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
    38.2 +++ b/src/Sequents/LK/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
    38.3 @@ -1,4 +1,4 @@
    38.4 -(*  Title:      LK/ex/ROOT.ML
    38.5 +(*  Title:      Sequents/LK/ROOT.ML
    38.6      ID:         $Id$
    38.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    38.8      Copyright   1992  University of Cambridge
    39.1 --- a/src/Sequents/modal.ML	Sat Sep 15 19:26:28 2007 +0200
    39.2 +++ b/src/Sequents/modal.ML	Sat Sep 15 19:27:35 2007 +0200
    39.3 @@ -1,4 +1,4 @@
    39.4 -(*  Title:      LK/modal.ML
    39.5 +(*  Title:      Sequents/modal.ML
    39.6      ID:         $Id$
    39.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    39.8      Copyright   1992  University of Cambridge
    40.1 --- a/src/Tools/Compute_Oracle/am_compiler.ML	Sat Sep 15 19:26:28 2007 +0200
    40.2 +++ b/src/Tools/Compute_Oracle/am_compiler.ML	Sat Sep 15 19:27:35 2007 +0200
    40.3 @@ -1,4 +1,4 @@
    40.4 -(*  Title:      Pure/Tools/am_compiler.ML
    40.5 +(*  Title:      Tools/Compute_Oracle/am_compiler.ML
    40.6      ID:         $Id$
    40.7      Author:     Steven Obua
    40.8  *)
    41.1 --- a/src/Tools/Compute_Oracle/am_ghc.ML	Sat Sep 15 19:26:28 2007 +0200
    41.2 +++ b/src/Tools/Compute_Oracle/am_ghc.ML	Sat Sep 15 19:27:35 2007 +0200
    41.3 @@ -1,4 +1,4 @@
    41.4 -(*  Title:      Pure/Tools/am_ghc.ML
    41.5 +(*  Title:      Tools/Compute_Oracle/am_ghc.ML
    41.6      ID:         $Id$
    41.7      Author:     Steven Obua
    41.8  *)
    42.1 --- a/src/Tools/Compute_Oracle/am_interpreter.ML	Sat Sep 15 19:26:28 2007 +0200
    42.2 +++ b/src/Tools/Compute_Oracle/am_interpreter.ML	Sat Sep 15 19:27:35 2007 +0200
    42.3 @@ -1,4 +1,4 @@
    42.4 -(*  Title:      Pure/Tools/am_interpreter.ML
    42.5 +(*  Title:      Tools/Compute_Oracle/am_interpreter.ML
    42.6      ID:         $Id$
    42.7      Author:     Steven Obua
    42.8  *)
    43.1 --- a/src/Tools/Compute_Oracle/am_sml.ML	Sat Sep 15 19:26:28 2007 +0200
    43.2 +++ b/src/Tools/Compute_Oracle/am_sml.ML	Sat Sep 15 19:27:35 2007 +0200
    43.3 @@ -1,4 +1,4 @@
    43.4 -(*  Title:      Pure/Tools/am_sml.ML
    43.5 +(*  Title:      Tools/Compute_Oracle/am_sml.ML
    43.6      ID:         $Id$
    43.7      Author:     Steven Obua
    43.8  
    44.1 --- a/src/Tools/Compute_Oracle/compute.ML	Sat Sep 15 19:26:28 2007 +0200
    44.2 +++ b/src/Tools/Compute_Oracle/compute.ML	Sat Sep 15 19:27:35 2007 +0200
    44.3 @@ -1,4 +1,4 @@
    44.4 -(*  Title:      Pure/Tools/compute.ML
    44.5 +(*  Title:      Tools/Compute_Oracle/compute.ML
    44.6      ID:         $Id$
    44.7      Author:     Steven Obua
    44.8  *)
    45.1 --- a/src/Tools/Compute_Oracle/linker.ML	Sat Sep 15 19:26:28 2007 +0200
    45.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Sat Sep 15 19:27:35 2007 +0200
    45.3 @@ -1,4 +1,4 @@
    45.4 -(*  Title:      Tools/Compute_Oracle/Linker.ML
    45.5 +(*  Title:      Tools/Compute_Oracle/linker.ML
    45.6      ID:         $Id$
    45.7      Author:     Steven Obua
    45.8  
    46.1 --- a/src/Tools/float.ML	Sat Sep 15 19:26:28 2007 +0200
    46.2 +++ b/src/Tools/float.ML	Sat Sep 15 19:27:35 2007 +0200
    46.3 @@ -1,4 +1,4 @@
    46.4 -(*  Title:      Pure/General/float.ML
    46.5 +(*  Title:      Tools/float.ML
    46.6      ID:         $Id$
    46.7      Author:     Steven Obua, Florian Haftmann, TU Muenchen
    46.8  
    47.1 --- a/src/Tools/integer.ML	Sat Sep 15 19:26:28 2007 +0200
    47.2 +++ b/src/Tools/integer.ML	Sat Sep 15 19:27:35 2007 +0200
    47.3 @@ -1,4 +1,4 @@
    47.4 -(*  Title:      Pure/General/int.ML
    47.5 +(*  Title:      Tools/integer.ML
    47.6      ID:         $Id$
    47.7      Author:     Florian Haftmann, TU Muenchen
    47.8  
    48.1 --- a/src/Tools/rat.ML	Sat Sep 15 19:26:28 2007 +0200
    48.2 +++ b/src/Tools/rat.ML	Sat Sep 15 19:27:35 2007 +0200
    48.3 @@ -1,4 +1,4 @@
    48.4 -(*  Title:      Pure/General/rat.ML
    48.5 +(*  Title:      Tools/rat.ML
    48.6      ID:         $Id$
    48.7      Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
    48.8  
    49.1 --- a/src/ZF/Coind/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
    49.2 +++ b/src/ZF/Coind/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
    49.3 @@ -1,4 +1,4 @@
    49.4 -(*  Title:      ZF/Coind/MT.ML
    49.5 +(*  Title:      ZF/Coind/ROOT.ML
    49.6      ID:         $Id$
    49.7      Author:     Jacob Frost, Cambridge University Computer Laboratory
    49.8      Copyright   1995  University of Cambridge
    50.1 --- a/src/ZF/Tools/cartprod.ML	Sat Sep 15 19:26:28 2007 +0200
    50.2 +++ b/src/ZF/Tools/cartprod.ML	Sat Sep 15 19:27:35 2007 +0200
    50.3 @@ -1,4 +1,4 @@
    50.4 -(*  Title:      ZF/cartprod.ML
    50.5 +(*  Title:      ZF/Tools/cartprod.ML
    50.6      ID:         $Id$
    50.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    50.8      Copyright   1996  University of Cambridge
    51.1 --- a/src/ZF/Tools/twos_compl.ML	Sat Sep 15 19:26:28 2007 +0200
    51.2 +++ b/src/ZF/Tools/twos_compl.ML	Sat Sep 15 19:27:35 2007 +0200
    51.3 @@ -1,4 +1,4 @@
    51.4 -(*  Title:      ZF/ex/twos-compl.ML
    51.5 +(*  Title:      ZF/Tools/twos_compl.ML
    51.6      ID:         $Id$
    51.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    51.8      Copyright   1993  University of Cambridge