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