--- a/src/FOLP/classical.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/FOLP/classical.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: FOLP/classical
+(* Title: FOLP/classical.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
--- a/src/FOLP/hypsubst.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/FOLP/hypsubst.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: FOLP/hypsubst
+(* Title: FOLP/hypsubst.ML
Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(* Author: Amine Chaieb
+(* Title: HOL/Decision_Procs/commutative_ring_tac.ML
+ Author: Amine Chaieb
Tactic for solving equalities over commutative rings.
*)
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Qelim/ferrante_rackoff.ML
+(* Title: HOL/Decision_Procs/ferrante_rackoff.ML
Author: Amine Chaieb, TU Muenchen
Ferrante and Rackoff's algorithm for quantifier elimination in dense
--- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Qelim/ferrante_rackoff_data.ML
+(* Title: HOL/Decision_Procs/ferrante_rackoff_data.ML
Author: Amine Chaieb, TU Muenchen
Context data for Ferrante and Rackoff's algorithm for quantifier
--- a/src/HOL/Decision_Procs/langford.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Qelim/langford.ML
+(* Title: HOL/Decision_Procs/langford.ML
Author: Amine Chaieb, TU Muenchen
*)
--- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: positivstellensatz_tools.ML
+(* Title: HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML
Author: Philipp Meyer, TU Muenchen
Functions for generating a certificate from a positivstellensatz and vice versa
--- a/src/HOL/Library/reify_data.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Library/reify_data.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/reflection_data.ML
+(* Title: HOL/Library/reify_data.ML
Author: Amine Chaieb, TU Muenchen
Data for the reification and reflection methods.
--- a/src/HOL/Multivariate_Analysis/normarith.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: Library/normarith.ML
+(* Title: HOL/Multivariate_Analysis/normarith.ML
Author: Amine Chaieb, University of Cambridge
Simple decision procedure for linear problems in Euclidean space.
--- a/src/HOL/Mutabelle/mutabelle.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,5 +1,4 @@
-(*
- Title: HOL/Mutabelle/mutabelle.ML
+(* Title: HOL/Mutabelle/mutabelle.ML
Author: Veronika Ortner, TU Muenchen
Mutation of theorems
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,5 +1,4 @@
-(*
- Title: HOL/Mutabelle/mutabelle_extra.ML
+(* Title: HOL/Mutabelle/mutabelle_extra.ML
Author: Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen
Invokation of Counterexample generators
--- a/src/HOL/NSA/transfer.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/NSA/transfer.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,6 +1,5 @@
-(* Title : HOL/Hyperreal/transfer.ML
- ID : $Id$
- Author : Brian Huffman
+(* Title: HOL/NSA/transfer.ML
+ Author: Brian Huffman
Transfer principle tactic for nonstandard analysis.
*)
--- a/src/HOL/Tools/Function/function.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Function/fundef.ML
+(* Title: HOL/Tools/Function/function.ML
Author: Alexander Krauss, TU Muenchen
A package for general recursive function definitions.
--- a/src/HOL/Tools/Function/function_lib.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Function/fundef_lib.ML
+(* Title: HOL/Tools/Function/function_lib.ML
Author: Alexander Krauss, TU Muenchen
A package for general recursive function definitions.
--- a/src/HOL/Tools/Function/pat_completeness.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Function/pat_completeness.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Function/fundef_datatype.ML
+(* Title: HOL/Tools/Function/pat_completeness.ML
Author: Alexander Krauss, TU Muenchen
Method "pat_completeness" to prove completeness of datatype patterns.
--- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Quotient/quotient_def.thy
+(* Title: HOL/Tools/Quotient/quotient_def.ML
Author: Cezary Kaliszyk and Christian Urban
Definitions for constants on quotient types.
--- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Quotient/quotient_info.thy
+(* Title: HOL/Tools/Quotient/quotient_info.ML
Author: Cezary Kaliszyk and Christian Urban
Data slots for the quotient package.
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Quotient/quotient_tacs.thy
+(* Title: HOL/Tools/Quotient/quotient_tacs.ML
Author: Cezary Kaliszyk and Christian Urban
Tactics for solving goal arising from lifting theorems to quotient
--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Quotient/quotient_term.thy
+(* Title: HOL/Tools/Quotient/quotient_term.ML
Author: Cezary Kaliszyk and Christian Urban
Constructs terms corresponding to goals from lifting theorems to
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Quotient/quotient_typ.thy
+(* Title: HOL/Tools/Quotient/quotient_typ.ML
Author: Cezary Kaliszyk and Christian Urban
Definition of a quotient type.
--- a/src/HOL/Tools/float_syntax.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/float_syntax.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(* Author: Tobias Nipkow, TU Muenchen
+(* Title: HOL/Tools/float_syntax.ML
+ Author: Tobias Nipkow, TU Muenchen
Concrete syntax for floats.
*)
--- a/src/HOL/Tools/groebner.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/groebner.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Groebner_Basis/groebner.ML
+(* Title: HOL/Tools/groebner.ML
Author: Amine Chaieb, TU Muenchen
*)
--- a/src/HOL/Tools/hologic.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/hologic.ML
+(* Title: HOL/Tools/hologic.ML
Author: Lawrence C Paulson and Markus Wenzel
Abstract syntax operations for HOL.
--- a/src/HOL/Tools/list_code.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/list_code.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(* Author: Florian Haftmann, TU Muenchen
+(* Title: HOL/Tools/list_code.ML
+ Author: Florian Haftmann, TU Muenchen
Code generation for list literals.
*)
--- a/src/HOL/Tools/quickcheck_generators.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(* Author: Florian Haftmann, TU Muenchen
+(* Title: HOL/Tools/quickcheck_generators.ML
+ Author: Florian Haftmann, TU Muenchen
Quickcheck generators for various types.
*)
--- a/src/HOL/Tools/semiring_normalizer.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Groebner_Basis/normalizer.ML
+(* Title: HOL/Tools/semiring_normalizer.ML
Author: Amine Chaieb, TU Muenchen
Normalization of expressions in semirings.
--- a/src/HOL/Tools/simpdata.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/simpdata.ML
+(* Title: HOL/Tools/simpdata.ML
Author: Tobias Nipkow
Copyright 1991 University of Cambridge
--- a/src/HOL/Tools/string_code.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/string_code.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(* Author: Florian Haftmann, TU Muenchen
+(* Title: HOL/Tools/string_code.ML
+ Author: Florian Haftmann, TU Muenchen
Code generation for character and string literals.
*)
--- a/src/HOL/Tools/transfer.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/transfer.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,6 +1,7 @@
-(* Author: Amine Chaieb, University of Cambridge, 2009
- Jeremy Avigad, Carnegie Mellon University
- Florian Haftmann, TU Muenchen
+(* Title: HOL/Tools/transfer.ML
+ Author: Amine Chaieb, University of Cambridge, 2009
+ Jeremy Avigad, Carnegie Mellon University
+ Florian Haftmann, TU Muenchen
Simple transfer principle on theorems.
*)
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOLCF/Tools/domain/domain_constructors.ML
+(* Title: HOLCF/Tools/Domain/domain_constructors.ML
Author: Brian Huffman
Defines constructor functions for a given domain isomorphism
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOLCF/Tools/domain/domain_isomorphism.ML
+(* Title: HOLCF/Tools/Domain/domain_isomorphism.ML
Author: Brian Huffman
Defines new types satisfying the given domain equations.
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOLCF/Tools/domain/domain_take_proofs.ML
+(* Title: HOLCF/Tools/Domain/domain_take_proofs.ML
Author: Brian Huffman
Defines take functions for the given domain equation
--- a/src/Provers/order.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Provers/order.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(* Author: Oliver Kutter, TU Muenchen
+(* Title: Provers/order.ML
+ Author: Oliver Kutter, TU Muenchen
Transitivity reasoner for partial and linear orders.
*)
--- a/src/Provers/quasi.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Provers/quasi.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(* Author: Oliver Kutter, TU Muenchen
+(* Title: Provers/quasi.ML
+ Author: Oliver Kutter, TU Muenchen
Reasoner for simple transitivity and quasi orders.
*)
--- a/src/Provers/trancl.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Provers/trancl.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,6 +1,7 @@
-(*
- Title: Transitivity reasoner for transitive closures of relations
+(* Title: Provers/trancl.ML
Author: Oliver Kutter, TU Muenchen
+
+Transitivity reasoner for transitive closures of relations
*)
(*
--- a/src/Tools/Code/code_eval.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: Tools/code/code_eval.ML
+(* Title: Tools/Code/code_eval.ML
Author: Florian Haftmann, TU Muenchen
Runtime services building on code generation into implementation language SML.
--- a/src/Tools/Code/code_preproc.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: Tools/code/code_preproc.ML
+(* Title: Tools/Code/code_preproc.ML
Author: Florian Haftmann, TU Muenchen
Preprocessing code equations into a well-sorted system
--- a/src/Tools/Code/code_printer.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: Tools/code/code_printer.ML
+(* Title: Tools/Code/code_printer.ML
Author: Florian Haftmann, TU Muenchen
Generic operations for pretty printing of target language code.
--- a/src/Tools/Code/code_simp.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/Code/code_simp.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: Tools/code/code_simp.ML
+(* Title: Tools/Code/code_simp.ML
Author: Florian Haftmann, TU Muenchen
Connecting the simplifier and the code generator.
--- a/src/Tools/Code/code_thingol.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: Tools/code/code_thingol.ML
+(* Title: Tools/Code/code_thingol.ML
Author: Florian Haftmann, TU Muenchen
Intermediate language ("Thin-gol") representing executable code.
--- a/src/Tools/WWW_Find/html_unicode.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/WWW_Find/html_unicode.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: html_unicode.ML
+(* Title: Tools/WWW_Find/html_unicode.ML
Author: Timothy Bourke, NICTA
Based on Pure/Thy/html.ML
by Markus Wenzel and Stefan Berghofer, TU Muenchen
--- a/src/Tools/value.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/Tools/value.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: Pure/Tools/value.ML
+(* Title: Tools/value.ML
Author: Florian Haftmann, TU Muenchen
Generic value command for arbitrary evaluators.