Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed title
authorhaftmann
Sat, 15 Sep 2007 19:27:35 +0200
changeset 24584 01e83ffa6c54
parent 24583 d77e4d48e497
child 24585 c359896d0f48
fixed title
Admin/de_overload.ML file | annotate | diff | comparison | revisions
doc-src/AxClass/Nat/NatClass.ML file | annotate | diff | comparison | revisions
doc-src/antiquote_setup.ML file | annotate | diff | comparison | revisions
src/FOLP/FOLP_lemmas.ML file | annotate | diff | comparison | revisions
src/FOLP/ex/Nat.ML file | annotate | diff | comparison | revisions
src/FOLP/ex/Prolog.ML file | annotate | diff | comparison | revisions
src/FOLP/intprover.ML file | annotate | diff | comparison | revisions
src/HOL/Hoare/ROOT.ML file | annotate | diff | comparison | revisions
src/HOL/Import/xml.ML file | annotate | diff | comparison | revisions
src/HOL/Matrix/cplex/matrixlp.ML file | annotate | diff | comparison | revisions
src/HOL/Nominal/ROOT.ML file | annotate | diff | comparison | revisions
src/HOL/Real/float_arith.ML file | annotate | diff | comparison | revisions
src/HOL/TLA/ROOT.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Qelim/cooper.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Qelim/cooper_data.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Qelim/ferrante_rackoff.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Qelim/ferrante_rackoff_data.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Qelim/generated_cooper.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Qelim/presburger.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/function_package/fundef_lib.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/function_package/pattern_split.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/inductive_codegen.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/recfun_codegen.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/split_rule.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/watcher.ML file | annotate | diff | comparison | revisions
src/HOL/ex/svc_funcs.ML file | annotate | diff | comparison | revisions
src/HOLCF/IOA/ABP/ROOT.ML file | annotate | diff | comparison | revisions
src/HOLCF/IOA/NTP/ROOT.ML file | annotate | diff | comparison | revisions
src/HOLCF/IOA/ROOT.ML file | annotate | diff | comparison | revisions
src/HOLCF/IOA/Storage/ROOT.ML file | annotate | diff | comparison | revisions
src/HOLCF/IOA/ex/ROOT.ML file | annotate | diff | comparison | revisions
src/Provers/Arith/abel_cancel.ML file | annotate | diff | comparison | revisions
src/Pure/General/xml.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/overloading_smlnj.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/polyml-5.1.ML file | annotate | diff | comparison | revisions
src/Pure/ProofGeneral/pgml.ML file | annotate | diff | comparison | revisions
src/Pure/Thy/html.ML file | annotate | diff | comparison | revisions
src/Sequents/LK/ROOT.ML file | annotate | diff | comparison | revisions
src/Sequents/modal.ML file | annotate | diff | comparison | revisions
src/Tools/Compute_Oracle/am_compiler.ML file | annotate | diff | comparison | revisions
src/Tools/Compute_Oracle/am_ghc.ML file | annotate | diff | comparison | revisions
src/Tools/Compute_Oracle/am_interpreter.ML file | annotate | diff | comparison | revisions
src/Tools/Compute_Oracle/am_sml.ML file | annotate | diff | comparison | revisions
src/Tools/Compute_Oracle/compute.ML file | annotate | diff | comparison | revisions
src/Tools/Compute_Oracle/linker.ML file | annotate | diff | comparison | revisions
src/Tools/float.ML file | annotate | diff | comparison | revisions
src/Tools/integer.ML file | annotate | diff | comparison | revisions
src/Tools/rat.ML file | annotate | diff | comparison | revisions
src/ZF/Coind/ROOT.ML file | annotate | diff | comparison | revisions
src/ZF/Tools/cartprod.ML file | annotate | diff | comparison | revisions
src/ZF/Tools/twos_compl.ML file | annotate | diff | comparison | revisions 
--- 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
 
--- 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
 
--- 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
 
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
 
--- 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
 *)
--- 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
 
--- 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
 *)
 
--- 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.
--- 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
 *)
--- 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
 *)
--- 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
 
--- 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
 
--- 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.
--- 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
 *)
--- 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
 
--- 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
 
--- 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
 
--- 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
 
--- 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
 
--- 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
--- 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
--- 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
 
--- 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
 
--- 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
 
--- 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
 
--- 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
 *)
--- 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
--- 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
 
--- 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
 
--- 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.
--- 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
 
--- 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
 
--- 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
--- 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
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 
--- 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
 *)
--- 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
 
--- 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
 
--- 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
 
--- 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
 
--- 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
--- 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
--- 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
isabelle