# HG changeset patch
# User haftmann
# Date 1189877255 -7200
# Node ID 01e83ffa6c542f8ff51abbbb1a2a0f0dcbcb2391
# Parent  d77e4d48e497230fcaa943560754d696906100c3
fixed title

diff -r d77e4d48e497 -r 01e83ffa6c54 Admin/de_overload.ML
--- a/Admin/de_overload.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/Admin/de_overload.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/ML-Systems/de_overload.ML
+(*  Title:      Admin/de_overload.ML
     ID:         $Id$
     Author:     Makarius
 
diff -r d77e4d48e497 -r 01e83ffa6c54 doc-src/AxClass/Nat/NatClass.ML
--- a/doc-src/AxClass/Nat/NatClass.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/doc-src/AxClass/Nat/NatClass.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      FOL/ex/NatClass.ML
+(*  Title:      Doc/AxClass/Nat/NatClass.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
diff -r d77e4d48e497 -r 01e83ffa6c54 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/doc-src/antiquote_setup.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      antiquote_setup.ML
+(*  Title:      Doc/antiquote_setup.ML
     ID:         $Id$
     Author:     Makarius
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/FOLP/FOLP_lemmas.ML
--- a/src/FOLP/FOLP_lemmas.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/FOLP/FOLP_lemmas.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      FOLP/FOLP.ML
+(*  Title:      FOLP/FOLP_lemmas.ML
     ID:         $Id$
     Author:     Martin D Coen, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
diff -r d77e4d48e497 -r 01e83ffa6c54 src/FOLP/ex/Nat.ML
--- a/src/FOLP/ex/Nat.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/FOLP/ex/Nat.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      FOLP/ex/nat.ML
+(*  Title:      FOLP/ex/Nat.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
diff -r d77e4d48e497 -r 01e83ffa6c54 src/FOLP/ex/Prolog.ML
--- a/src/FOLP/ex/Prolog.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/FOLP/ex/Prolog.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      FOLP/ex/prolog.ML
+(*  Title:      FOLP/ex/Prolog.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
diff -r d77e4d48e497 -r 01e83ffa6c54 src/FOLP/intprover.ML
--- a/src/FOLP/intprover.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/FOLP/intprover.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      FOLP/int-prover.ML
+(*  Title:      FOLP/intprover.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Hoare/ROOT.ML
--- a/src/HOL/Hoare/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Hoare/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IMP/ROOT.ML
+(*  Title:      HOL/Hoare/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1998-2003 TUM
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Import/xml.ML
--- a/src/HOL/Import/xml.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Import/xml.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/General/xml.ML
+(*  Title:      HOL/Import/xml.ML
     ID:         $Id$
     Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Matrix/cplex/matrixlp.ML
--- a/src/HOL/Matrix/cplex/matrixlp.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Matrix/cplex/matrixlp.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/cplex/MatrixLP.ML
+(*  Title:      HOL/Matrix/cplex/matrixlp.ML
     ID:         $Id$
     Author:     Steven Obua
 *)
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Nominal/ROOT.ML
--- a/src/HOL/Nominal/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Nominal/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Nominal/nominal_atoms.ML
+(*  Title:      HOL/Nominal/ROOT.ML
     ID:         $Id$
     Author:     Stefan Berghofer and Christian Urban, TU Muenchen
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Real/float_arith.ML
--- a/src/HOL/Real/float_arith.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Real/float_arith.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,5 +1,5 @@
-(*  Title: HOL/Real/Float.ML
-    ID:    $Id$
+(*  Title:  HOL/Real/float_arith.ML
+    ID:     $Id$
     Author: Steven Obua
 *)
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/TLA/ROOT.ML
--- a/src/HOL/TLA/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/TLA/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      TLA/ROOT.ML
+(*  Title:      HOL/TLA/ROOT.ML
     ID:         $Id$
 
 Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Presburger/cooper.ML
+(*  Title:      HOL/Tools/Qelim/cooper.ML
     ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Tools/Qelim/cooper_data.ML
--- a/src/HOL/Tools/Qelim/cooper_data.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper_data.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Presburger/cooper_data.ML
+(*  Title:      HOL/Tools/Qelim/cooper_data.ML
     ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Tools/Qelim/ferrante_rackoff.ML
--- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(* Title:      HOL/Tools/ferrante_rackoff.ML
+(* Title:      HOL/Tools/Qelim/ferrante_rackoff.ML
    ID:         $Id$
    Author:     Amine Chaieb, TU Muenchen
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Tools/Qelim/ferrante_rackoff_data.ML
--- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(* Title:      HOL/Tools/ferrante_rackoff_data.ML
+(* Title:      HOL/Tools/Qelim/ferrante_rackoff_data.ML
    ID:         $Id$
    Author:     Amine Chaieb, TU Muenchen
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Tools/Qelim/generated_cooper.ML
--- a/src/HOL/Tools/Qelim/generated_cooper.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Tools/Qelim/generated_cooper.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Presburger/generated_cooper.ML
+(*  Title:      HOL/Tools/Qelim/generated_cooper.ML
     ID:         $Id$
 
 This file is generated from HOL/ex/Reflected_Presburger.thy.  DO NOT EDIT.
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Presburger/presburger.ML
+(*  Title:      HOL/Tools/Qelim/presburger.ML
     ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Tools/function_package/fundef_lib.ML
--- a/src/HOL/Tools/function_package/fundef_lib.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/function_package/lib.ML
+(*  Title:      HOL/Tools/function_package/fundef_lib.ML
     ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Tools/function_package/pattern_split.ML
--- a/src/HOL/Tools/function_package/pattern_split.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Tools/function_package/pattern_split.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/function_package/fundef_package.ML
+(*  Title:      HOL/Tools/function_package/pattern_split.ML
     ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/inductive_codegen.ML
+(*  Title:      HOL/Tools/inductive_codegen.ML
     ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/recfun_codegen.ML
+(*  Title:      HOL/Tools/recfun_codegen.ML
     ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Tools/split_rule.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Tools/split_rule.ML
+(*  Title:      HOL/Tools/split_rule.ML
     ID:         $Id$
     Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/Tools/watcher.ML
--- a/src/HOL/Tools/watcher.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/Tools/watcher.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Watcher.ML
+(*  Title:      HOL/Tools/watcher.ML
     ID:         $Id$
     Author:     Claire Quigley
     Copyright   2004  University of Cambridge
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/svc_funcs.ML
+(*  Title:      HOL/ex/svc_funcs.ML
     ID:         $Id$
     Author:     Lawrence C Paulson
     Copyright   1999  University of Cambridge
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOLCF/IOA/ABP/ROOT.ML
--- a/src/HOLCF/IOA/ABP/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOLCF/IOA/ABP/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/ABP/ROOT.ML
+(*  Title:      HOLCF/IOA/ABP/ROOT.ML
     ID:         $Id$
     Author:     Olaf Mueller
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOLCF/IOA/NTP/ROOT.ML
--- a/src/HOLCF/IOA/NTP/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOLCF/IOA/NTP/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/examples/NTP/ROOT.ML
+(*  Title:      HOLCF/IOA/NTP/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow & Konrad Slind
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOLCF/IOA/ROOT.ML
--- a/src/HOLCF/IOA/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOLCF/IOA/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/ROOT.ML
+(*  Title:      HOLCF/IOA/ROOT.ML
     ID:         $Id$
     Author:     Olaf Mueller
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOLCF/IOA/Storage/ROOT.ML
--- a/src/HOLCF/IOA/Storage/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOLCF/IOA/Storage/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/Storage/ROOT.ML
+(*  Title:      HOLCF/IOA/Storage/ROOT.ML
     ID:         $Id$
     Author:     Olaf Mueller
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/HOLCF/IOA/ex/ROOT.ML
--- a/src/HOLCF/IOA/ex/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/HOLCF/IOA/ex/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/ex/ROOT.ML
+(*  Title:      HOLCF/IOA/ex/ROOT.ML
     ID:         $Id$
     Author:     Olaf Mueller
 *)
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/OrderedGroup.ML
+(*  Title:      Provers/Arith/abel_cancel.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Pure/General/xml.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/Tools/xml.ML
+(*  Title:      Pure/General/xml.ML
     ID:         $Id$
     Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Pure/ML-Systems/overloading_smlnj.ML
--- a/src/Pure/ML-Systems/overloading_smlnj.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Pure/ML-Systems/overloading_smlnj.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/ML-Systems/overloading-smlnj.ML
+(*  Title:      Pure/ML-Systems/overloading_smlnj.ML
     ID:         $Id$
     Author:     Makarius
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Pure/ML-Systems/polyml-5.1.ML
--- a/src/Pure/ML-Systems/polyml-5.1.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/ML-Systems/polyml-5.0.ML
+(*  Title:      Pure/ML-Systems/polyml-5.1.ML
     ID:         $Id$
 
 Compatibility wrapper for Poly/ML 5.1.
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Pure/ProofGeneral/pgml.ML
--- a/src/Pure/ProofGeneral/pgml.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Pure/ProofGeneral/pgml.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/ProofGeneral/pgip_types.ML
+(*  Title:      Pure/ProofGeneral/pgml.ML
     ID:         $Id$
     Author:     David Aspinall
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Pure/Thy/html.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/Thy/HTML.ML
+(*  Title:      Pure/Thy/html.ML
     ID:         $Id$
     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Sequents/LK/ROOT.ML
--- a/src/Sequents/LK/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Sequents/LK/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      LK/ex/ROOT.ML
+(*  Title:      Sequents/LK/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Sequents/modal.ML
--- a/src/Sequents/modal.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Sequents/modal.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      LK/modal.ML
+(*  Title:      Sequents/modal.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Tools/Compute_Oracle/am_compiler.ML
--- a/src/Tools/Compute_Oracle/am_compiler.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Tools/Compute_Oracle/am_compiler.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/Tools/am_compiler.ML
+(*  Title:      Tools/Compute_Oracle/am_compiler.ML
     ID:         $Id$
     Author:     Steven Obua
 *)
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Tools/Compute_Oracle/am_ghc.ML
--- a/src/Tools/Compute_Oracle/am_ghc.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Tools/Compute_Oracle/am_ghc.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/Tools/am_ghc.ML
+(*  Title:      Tools/Compute_Oracle/am_ghc.ML
     ID:         $Id$
     Author:     Steven Obua
 *)
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Tools/Compute_Oracle/am_interpreter.ML
--- a/src/Tools/Compute_Oracle/am_interpreter.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Tools/Compute_Oracle/am_interpreter.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/Tools/am_interpreter.ML
+(*  Title:      Tools/Compute_Oracle/am_interpreter.ML
     ID:         $Id$
     Author:     Steven Obua
 *)
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Tools/Compute_Oracle/am_sml.ML
--- a/src/Tools/Compute_Oracle/am_sml.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Tools/Compute_Oracle/am_sml.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/Tools/am_sml.ML
+(*  Title:      Tools/Compute_Oracle/am_sml.ML
     ID:         $Id$
     Author:     Steven Obua
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Tools/Compute_Oracle/compute.ML
--- a/src/Tools/Compute_Oracle/compute.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Tools/Compute_Oracle/compute.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/Tools/compute.ML
+(*  Title:      Tools/Compute_Oracle/compute.ML
     ID:         $Id$
     Author:     Steven Obua
 *)
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Tools/Compute_Oracle/linker.ML
--- a/src/Tools/Compute_Oracle/linker.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Tools/Compute_Oracle/linker.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Tools/Compute_Oracle/Linker.ML
+(*  Title:      Tools/Compute_Oracle/linker.ML
     ID:         $Id$
     Author:     Steven Obua
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Tools/float.ML
--- a/src/Tools/float.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Tools/float.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/General/float.ML
+(*  Title:      Tools/float.ML
     ID:         $Id$
     Author:     Steven Obua, Florian Haftmann, TU Muenchen
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Tools/integer.ML
--- a/src/Tools/integer.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Tools/integer.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/General/int.ML
+(*  Title:      Tools/integer.ML
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/Tools/rat.ML
--- a/src/Tools/rat.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/Tools/rat.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/General/rat.ML
+(*  Title:      Tools/rat.ML
     ID:         $Id$
     Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
 
diff -r d77e4d48e497 -r 01e83ffa6c54 src/ZF/Coind/ROOT.ML
--- a/src/ZF/Coind/ROOT.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/ZF/Coind/ROOT.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      ZF/Coind/MT.ML
+(*  Title:      ZF/Coind/ROOT.ML
     ID:         $Id$
     Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
diff -r d77e4d48e497 -r 01e83ffa6c54 src/ZF/Tools/cartprod.ML
--- a/src/ZF/Tools/cartprod.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/ZF/Tools/cartprod.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      ZF/cartprod.ML
+(*  Title:      ZF/Tools/cartprod.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
diff -r d77e4d48e497 -r 01e83ffa6c54 src/ZF/Tools/twos_compl.ML
--- a/src/ZF/Tools/twos_compl.ML	Sat Sep 15 19:26:28 2007 +0200
+++ b/src/ZF/Tools/twos_compl.ML	Sat Sep 15 19:27:35 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      ZF/ex/twos-compl.ML
+(*  Title:      ZF/Tools/twos_compl.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge