1.1 --- a/src/FOLP/classical.ML	Thu Jul 08 16:19:23 2010 +0200
     1.2 +++ b/src/FOLP/classical.ML	Thu Jul 08 16:19:24 2010 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      FOLP/classical
     1.5 +(*  Title:      FOLP/classical.ML
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1992  University of Cambridge
     1.8  

     2.1 --- a/src/FOLP/hypsubst.ML	Thu Jul 08 16:19:23 2010 +0200
     2.2 +++ b/src/FOLP/hypsubst.ML	Thu Jul 08 16:19:24 2010 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      FOLP/hypsubst
     2.5 +(*  Title:      FOLP/hypsubst.ML
     2.6      Author:     Martin D Coen, Cambridge University Computer Laboratory
     2.7      Copyright   1995  University of Cambridge
     2.8  

     3.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Jul 08 16:19:23 2010 +0200
     3.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Jul 08 16:19:24 2010 +0200
     3.3 @@ -1,4 +1,5 @@
     3.4 -(*  Author:     Amine Chaieb
     3.5 +(*  Title:      HOL/Decision_Procs/commutative_ring_tac.ML
     3.6 +    Author:     Amine Chaieb
     3.7  
     3.8  Tactic for solving equalities over commutative rings.
     3.9  *)

     4.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Jul 08 16:19:23 2010 +0200
     4.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Jul 08 16:19:24 2010 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(* Title:      HOL/Tools/Qelim/ferrante_rackoff.ML
     4.5 +(* Title:      HOL/Decision_Procs/ferrante_rackoff.ML
     4.6     Author:     Amine Chaieb, TU Muenchen
     4.7  
     4.8  Ferrante and Rackoff's algorithm for quantifier elimination in dense

     5.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML	Thu Jul 08 16:19:23 2010 +0200
     5.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML	Thu Jul 08 16:19:24 2010 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -(* Title:      HOL/Tools/Qelim/ferrante_rackoff_data.ML
     5.5 +(* Title:      HOL/Decision_Procs/ferrante_rackoff_data.ML
     5.6     Author:     Amine Chaieb, TU Muenchen
     5.7  
     5.8  Context data for Ferrante and Rackoff's algorithm for quantifier

     6.1 --- a/src/HOL/Decision_Procs/langford.ML	Thu Jul 08 16:19:23 2010 +0200
     6.2 +++ b/src/HOL/Decision_Procs/langford.ML	Thu Jul 08 16:19:24 2010 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      HOL/Tools/Qelim/langford.ML
     6.5 +(*  Title:      HOL/Decision_Procs/langford.ML
     6.6      Author:     Amine Chaieb, TU Muenchen
     6.7  *)
     6.8  

     7.1 --- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Thu Jul 08 16:19:23 2010 +0200
     7.2 +++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Thu Jul 08 16:19:24 2010 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -(* Title:      positivstellensatz_tools.ML
     7.5 +(* Title:      HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML
     7.6     Author:     Philipp Meyer, TU Muenchen
     7.7  
     7.8  Functions for generating a certificate from a positivstellensatz and vice versa

     8.1 --- a/src/HOL/Library/reify_data.ML	Thu Jul 08 16:19:23 2010 +0200
     8.2 +++ b/src/HOL/Library/reify_data.ML	Thu Jul 08 16:19:24 2010 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOL/Library/reflection_data.ML
     8.5 +(*  Title:      HOL/Library/reify_data.ML
     8.6      Author:     Amine Chaieb, TU Muenchen
     8.7  
     8.8  Data for the reification and reflection methods.

     9.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Thu Jul 08 16:19:23 2010 +0200
     9.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Thu Jul 08 16:19:24 2010 +0200
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      Library/normarith.ML
     9.5 +(*  Title:      HOL/Multivariate_Analysis/normarith.ML
     9.6      Author:     Amine Chaieb, University of Cambridge
     9.7  
     9.8  Simple decision procedure for linear problems in Euclidean space.

    10.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Thu Jul 08 16:19:23 2010 +0200
    10.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Thu Jul 08 16:19:24 2010 +0200
    10.3 @@ -1,5 +1,4 @@
    10.4 -(*
    10.5 -    Title:      HOL/Mutabelle/mutabelle.ML
    10.6 +(*  Title:      HOL/Mutabelle/mutabelle.ML
    10.7      Author:     Veronika Ortner, TU Muenchen
    10.8  
    10.9      Mutation of theorems

    11.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Jul 08 16:19:23 2010 +0200
    11.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Jul 08 16:19:24 2010 +0200
    11.3 @@ -1,5 +1,4 @@
    11.4 -(*
    11.5 -    Title:      HOL/Mutabelle/mutabelle_extra.ML
    11.6 +(*  Title:      HOL/Mutabelle/mutabelle_extra.ML
    11.7      Author:     Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen
    11.8  
    11.9      Invokation of Counterexample generators

    12.1 --- a/src/HOL/NSA/transfer.ML	Thu Jul 08 16:19:23 2010 +0200
    12.2 +++ b/src/HOL/NSA/transfer.ML	Thu Jul 08 16:19:24 2010 +0200
    12.3 @@ -1,6 +1,5 @@
    12.4 -(*  Title       : HOL/Hyperreal/transfer.ML
    12.5 -    ID          : $Id$
    12.6 -    Author      : Brian Huffman
    12.7 +(*  Title:      HOL/NSA/transfer.ML
    12.8 +    Author:     Brian Huffman
    12.9  
   12.10  Transfer principle tactic for nonstandard analysis.
   12.11  *)

    13.1 --- a/src/HOL/Tools/Function/function.ML	Thu Jul 08 16:19:23 2010 +0200
    13.2 +++ b/src/HOL/Tools/Function/function.ML	Thu Jul 08 16:19:24 2010 +0200
    13.3 @@ -1,4 +1,4 @@
    13.4 -(*  Title:      HOL/Tools/Function/fundef.ML
    13.5 +(*  Title:      HOL/Tools/Function/function.ML
    13.6      Author:     Alexander Krauss, TU Muenchen
    13.7  
    13.8  A package for general recursive function definitions.

    14.1 --- a/src/HOL/Tools/Function/function_lib.ML	Thu Jul 08 16:19:23 2010 +0200
    14.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Thu Jul 08 16:19:24 2010 +0200
    14.3 @@ -1,4 +1,4 @@
    14.4 -(*  Title:      HOL/Tools/Function/fundef_lib.ML
    14.5 +(*  Title:      HOL/Tools/Function/function_lib.ML
    14.6      Author:     Alexander Krauss, TU Muenchen
    14.7  
    14.8  A package for general recursive function definitions.

    15.1 --- a/src/HOL/Tools/Function/pat_completeness.ML	Thu Jul 08 16:19:23 2010 +0200
    15.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Thu Jul 08 16:19:24 2010 +0200
    15.3 @@ -1,4 +1,4 @@
    15.4 -(*  Title:      HOL/Tools/Function/fundef_datatype.ML
    15.5 +(*  Title:      HOL/Tools/Function/pat_completeness.ML
    15.6      Author:     Alexander Krauss, TU Muenchen
    15.7  
    15.8  Method "pat_completeness" to prove completeness of datatype patterns.

    16.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Jul 08 16:19:23 2010 +0200
    16.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Jul 08 16:19:24 2010 +0200
    16.3 @@ -1,4 +1,4 @@
    16.4 -(*  Title:      HOL/Tools/Quotient/quotient_def.thy
    16.5 +(*  Title:      HOL/Tools/Quotient/quotient_def.ML
    16.6      Author:     Cezary Kaliszyk and Christian Urban
    16.7  
    16.8  Definitions for constants on quotient types.

    17.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Jul 08 16:19:23 2010 +0200
    17.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Jul 08 16:19:24 2010 +0200
    17.3 @@ -1,4 +1,4 @@
    17.4 -(*  Title:      HOL/Tools/Quotient/quotient_info.thy
    17.5 +(*  Title:      HOL/Tools/Quotient/quotient_info.ML
    17.6      Author:     Cezary Kaliszyk and Christian Urban
    17.7  
    17.8  Data slots for the quotient package.

    18.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Jul 08 16:19:23 2010 +0200
    18.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Jul 08 16:19:24 2010 +0200
    18.3 @@ -1,4 +1,4 @@
    18.4 -(*  Title:      HOL/Tools/Quotient/quotient_tacs.thy
    18.5 +(*  Title:      HOL/Tools/Quotient/quotient_tacs.ML
    18.6      Author:     Cezary Kaliszyk and Christian Urban
    18.7  
    18.8  Tactics for solving goal arising from lifting theorems to quotient

    19.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jul 08 16:19:23 2010 +0200
    19.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jul 08 16:19:24 2010 +0200
    19.3 @@ -1,4 +1,4 @@
    19.4 -(*  Title:      HOL/Tools/Quotient/quotient_term.thy
    19.5 +(*  Title:      HOL/Tools/Quotient/quotient_term.ML
    19.6      Author:     Cezary Kaliszyk and Christian Urban
    19.7  
    19.8  Constructs terms corresponding to goals from lifting theorems to

    20.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Jul 08 16:19:23 2010 +0200
    20.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Jul 08 16:19:24 2010 +0200
    20.3 @@ -1,4 +1,4 @@
    20.4 -(*  Title:      HOL/Tools/Quotient/quotient_typ.thy
    20.5 +(*  Title:      HOL/Tools/Quotient/quotient_typ.ML
    20.6      Author:     Cezary Kaliszyk and Christian Urban
    20.7  
    20.8  Definition of a quotient type.

    21.1 --- a/src/HOL/Tools/float_syntax.ML	Thu Jul 08 16:19:23 2010 +0200
    21.2 +++ b/src/HOL/Tools/float_syntax.ML	Thu Jul 08 16:19:24 2010 +0200
    21.3 @@ -1,4 +1,5 @@
    21.4 -(*  Author:     Tobias Nipkow, TU Muenchen
    21.5 +(*  Title:      HOL/Tools/float_syntax.ML
    21.6 +    Author:     Tobias Nipkow, TU Muenchen
    21.7  
    21.8  Concrete syntax for floats.
    21.9  *)

    22.1 --- a/src/HOL/Tools/groebner.ML	Thu Jul 08 16:19:23 2010 +0200
    22.2 +++ b/src/HOL/Tools/groebner.ML	Thu Jul 08 16:19:24 2010 +0200
    22.3 @@ -1,4 +1,4 @@
    22.4 -(*  Title:      HOL/Tools/Groebner_Basis/groebner.ML
    22.5 +(*  Title:      HOL/Tools/groebner.ML
    22.6      Author:     Amine Chaieb, TU Muenchen
    22.7  *)
    22.8  

    23.1 --- a/src/HOL/Tools/hologic.ML	Thu Jul 08 16:19:23 2010 +0200
    23.2 +++ b/src/HOL/Tools/hologic.ML	Thu Jul 08 16:19:24 2010 +0200
    23.3 @@ -1,4 +1,4 @@
    23.4 -(*  Title:      HOL/hologic.ML
    23.5 +(*  Title:      HOL/Tools/hologic.ML
    23.6      Author:     Lawrence C Paulson and Markus Wenzel
    23.7  
    23.8  Abstract syntax operations for HOL.

    24.1 --- a/src/HOL/Tools/list_code.ML	Thu Jul 08 16:19:23 2010 +0200
    24.2 +++ b/src/HOL/Tools/list_code.ML	Thu Jul 08 16:19:24 2010 +0200
    24.3 @@ -1,4 +1,5 @@
    24.4 -(* Author: Florian Haftmann, TU Muenchen
    24.5 +(*  Title:  HOL/Tools/list_code.ML
    24.6 +    Author: Florian Haftmann, TU Muenchen
    24.7  
    24.8  Code generation for list literals.
    24.9  *)

    25.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Thu Jul 08 16:19:23 2010 +0200
    25.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Jul 08 16:19:24 2010 +0200
    25.3 @@ -1,4 +1,5 @@
    25.4 -(* Author: Florian Haftmann, TU Muenchen
    25.5 +(*  Title:      HOL/Tools/quickcheck_generators.ML
    25.6 +    Author:     Florian Haftmann, TU Muenchen
    25.7  
    25.8  Quickcheck generators for various types.
    25.9  *)

    26.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Thu Jul 08 16:19:23 2010 +0200
    26.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Thu Jul 08 16:19:24 2010 +0200
    26.3 @@ -1,4 +1,4 @@
    26.4 -(*  Title:      HOL/Tools/Groebner_Basis/normalizer.ML
    26.5 +(*  Title:      HOL/Tools/semiring_normalizer.ML
    26.6      Author:     Amine Chaieb, TU Muenchen
    26.7  
    26.8  Normalization of expressions in semirings.

    27.1 --- a/src/HOL/Tools/simpdata.ML	Thu Jul 08 16:19:23 2010 +0200
    27.2 +++ b/src/HOL/Tools/simpdata.ML	Thu Jul 08 16:19:24 2010 +0200
    27.3 @@ -1,4 +1,4 @@
    27.4 -(*  Title:      HOL/simpdata.ML
    27.5 +(*  Title:      HOL/Tools/simpdata.ML
    27.6      Author:     Tobias Nipkow
    27.7      Copyright   1991  University of Cambridge
    27.8  

    28.1 --- a/src/HOL/Tools/string_code.ML	Thu Jul 08 16:19:23 2010 +0200
    28.2 +++ b/src/HOL/Tools/string_code.ML	Thu Jul 08 16:19:24 2010 +0200
    28.3 @@ -1,4 +1,5 @@
    28.4 -(* Author: Florian Haftmann, TU Muenchen
    28.5 +(*  Title:      HOL/Tools/string_code.ML
    28.6 +    Author:     Florian Haftmann, TU Muenchen
    28.7  
    28.8  Code generation for character and string literals.
    28.9  *)

    29.1 --- a/src/HOL/Tools/transfer.ML	Thu Jul 08 16:19:23 2010 +0200
    29.2 +++ b/src/HOL/Tools/transfer.ML	Thu Jul 08 16:19:24 2010 +0200
    29.3 @@ -1,6 +1,7 @@
    29.4 -(*  Author:   Amine Chaieb, University of Cambridge, 2009
    29.5 -              Jeremy Avigad, Carnegie Mellon University
    29.6 -              Florian Haftmann, TU Muenchen
    29.7 +(*  Title:      HOL/Tools/transfer.ML
    29.8 +    Author:     Amine Chaieb, University of Cambridge, 2009
    29.9 +                Jeremy Avigad, Carnegie Mellon University
   29.10 +                Florian Haftmann, TU Muenchen
   29.11  
   29.12  Simple transfer principle on theorems.
   29.13  *)

    30.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jul 08 16:19:23 2010 +0200
    30.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jul 08 16:19:24 2010 +0200
    30.3 @@ -1,4 +1,4 @@
    30.4 -(*  Title:      HOLCF/Tools/domain/domain_constructors.ML
    30.5 +(*  Title:      HOLCF/Tools/Domain/domain_constructors.ML
    30.6      Author:     Brian Huffman
    30.7  
    30.8  Defines constructor functions for a given domain isomorphism

    31.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Jul 08 16:19:23 2010 +0200
    31.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Jul 08 16:19:24 2010 +0200
    31.3 @@ -1,4 +1,4 @@
    31.4 -(*  Title:      HOLCF/Tools/domain/domain_isomorphism.ML
    31.5 +(*  Title:      HOLCF/Tools/Domain/domain_isomorphism.ML
    31.6      Author:     Brian Huffman
    31.7  
    31.8  Defines new types satisfying the given domain equations.

    32.1 --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu Jul 08 16:19:23 2010 +0200
    32.2 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu Jul 08 16:19:24 2010 +0200
    32.3 @@ -1,4 +1,4 @@
    32.4 -(*  Title:      HOLCF/Tools/domain/domain_take_proofs.ML
    32.5 +(*  Title:      HOLCF/Tools/Domain/domain_take_proofs.ML
    32.6      Author:     Brian Huffman
    32.7  
    32.8  Defines take functions for the given domain equation

    33.1 --- a/src/Provers/order.ML	Thu Jul 08 16:19:23 2010 +0200
    33.2 +++ b/src/Provers/order.ML	Thu Jul 08 16:19:24 2010 +0200
    33.3 @@ -1,4 +1,5 @@
    33.4 -(*  Author:     Oliver Kutter, TU Muenchen
    33.5 +(*  Title:      Provers/order.ML
    33.6 +    Author:     Oliver Kutter, TU Muenchen
    33.7  
    33.8  Transitivity reasoner for partial and linear orders.
    33.9  *)

    34.1 --- a/src/Provers/quasi.ML	Thu Jul 08 16:19:23 2010 +0200
    34.2 +++ b/src/Provers/quasi.ML	Thu Jul 08 16:19:24 2010 +0200
    34.3 @@ -1,4 +1,5 @@
    34.4 -(*  Author:     Oliver Kutter, TU Muenchen
    34.5 +(*  Title:      Provers/quasi.ML
    34.6 +    Author:     Oliver Kutter, TU Muenchen
    34.7  
    34.8  Reasoner for simple transitivity and quasi orders.
    34.9  *)

    35.1 --- a/src/Provers/trancl.ML	Thu Jul 08 16:19:23 2010 +0200
    35.2 +++ b/src/Provers/trancl.ML	Thu Jul 08 16:19:24 2010 +0200
    35.3 @@ -1,6 +1,7 @@
    35.4 -(*
    35.5 -    Title:      Transitivity reasoner for transitive closures of relations
    35.6 +(*  Title:      Provers/trancl.ML
    35.7      Author:     Oliver Kutter, TU Muenchen
    35.8 +
    35.9 +Transitivity reasoner for transitive closures of relations
   35.10  *)
   35.11  
   35.12  (*

    36.1 --- a/src/Tools/Code/code_eval.ML	Thu Jul 08 16:19:23 2010 +0200
    36.2 +++ b/src/Tools/Code/code_eval.ML	Thu Jul 08 16:19:24 2010 +0200
    36.3 @@ -1,4 +1,4 @@
    36.4 -(*  Title:      Tools/code/code_eval.ML
    36.5 +(*  Title:      Tools/Code/code_eval.ML
    36.6      Author:     Florian Haftmann, TU Muenchen
    36.7  
    36.8  Runtime services building on code generation into implementation language SML.

    37.1 --- a/src/Tools/Code/code_preproc.ML	Thu Jul 08 16:19:23 2010 +0200
    37.2 +++ b/src/Tools/Code/code_preproc.ML	Thu Jul 08 16:19:24 2010 +0200
    37.3 @@ -1,4 +1,4 @@
    37.4 -(*  Title:      Tools/code/code_preproc.ML
    37.5 +(*  Title:      Tools/Code/code_preproc.ML
    37.6      Author:     Florian Haftmann, TU Muenchen
    37.7  
    37.8  Preprocessing code equations into a well-sorted system

    38.1 --- a/src/Tools/Code/code_printer.ML	Thu Jul 08 16:19:23 2010 +0200
    38.2 +++ b/src/Tools/Code/code_printer.ML	Thu Jul 08 16:19:24 2010 +0200
    38.3 @@ -1,4 +1,4 @@
    38.4 -(*  Title:      Tools/code/code_printer.ML
    38.5 +(*  Title:      Tools/Code/code_printer.ML
    38.6      Author:     Florian Haftmann, TU Muenchen
    38.7  
    38.8  Generic operations for pretty printing of target language code.

    39.1 --- a/src/Tools/Code/code_simp.ML	Thu Jul 08 16:19:23 2010 +0200
    39.2 +++ b/src/Tools/Code/code_simp.ML	Thu Jul 08 16:19:24 2010 +0200
    39.3 @@ -1,4 +1,4 @@
    39.4 -(*  Title:      Tools/code/code_simp.ML
    39.5 +(*  Title:      Tools/Code/code_simp.ML
    39.6      Author:     Florian Haftmann, TU Muenchen
    39.7  
    39.8  Connecting the simplifier and the code generator.

    40.1 --- a/src/Tools/Code/code_thingol.ML	Thu Jul 08 16:19:23 2010 +0200
    40.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Jul 08 16:19:24 2010 +0200
    40.3 @@ -1,4 +1,4 @@
    40.4 -(*  Title:      Tools/code/code_thingol.ML
    40.5 +(*  Title:      Tools/Code/code_thingol.ML
    40.6      Author:     Florian Haftmann, TU Muenchen
    40.7  
    40.8  Intermediate language ("Thin-gol") representing executable code.

    41.1 --- a/src/Tools/WWW_Find/html_unicode.ML	Thu Jul 08 16:19:23 2010 +0200
    41.2 +++ b/src/Tools/WWW_Find/html_unicode.ML	Thu Jul 08 16:19:24 2010 +0200
    41.3 @@ -1,4 +1,4 @@
    41.4 -(*  Title:      html_unicode.ML
    41.5 +(*  Title:      Tools/WWW_Find/html_unicode.ML
    41.6      Author:     Timothy Bourke, NICTA
    41.7                  Based on Pure/Thy/html.ML
    41.8                  by Markus Wenzel and Stefan Berghofer, TU Muenchen

    42.1 --- a/src/Tools/value.ML	Thu Jul 08 16:19:23 2010 +0200
    42.2 +++ b/src/Tools/value.ML	Thu Jul 08 16:19:24 2010 +0200
    42.3 @@ -1,4 +1,4 @@
    42.4 -(*  Title:      Pure/Tools/value.ML
    42.5 +(*  Title:      Tools/value.ML
    42.6      Author:     Florian Haftmann, TU Muenchen
    42.7  
    42.8  Generic value command for arbitrary evaluators.