proper file headers;

--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/positivstellensatz.ML
+(*  Title:      HOL/Library/Sum_of_Squares/positivstellensatz.ML
     Author:     Amine Chaieb, University of Cambridge
 
 A generic arithmetic prover based on Positivstellensatz certificates

--- a/src/HOL/Library/Tools/smt_word.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Library/Tools/smt_word.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Word/Tools/smt_word.ML
+(*  Title:      HOL/Library/Tools/smt_word.ML
     Author:     Sascha Boehme, TU Muenchen
 
 SMT setup for words.

--- a/src/HOL/Library/Tools/word_lib.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Library/Tools/word_lib.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Word/Tools/word_lib.ML
+(*  Title:      HOL/Library/Tools/word_lib.ML
     Author:     Sascha Boehme, TU Muenchen and Thomas Sewell, NICTA
 
 Helper routines for operating on the word type.

--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Mirabelle/Tools/mirabelle.ML
+(*  Title:      HOL/Tools/Mirabelle/mirabelle.ML
     Author:     Jasmin Blanchette, TU Munich
     Author:     Sascha Boehme, TU Munich
     Author:     Makarius

--- a/src/HOL/Tools/Mirabelle/mirabelle_arith.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Mirabelle/Tools/mirabelle_arith.ML
+(*  Title:      HOL/Tools/Mirabelle/mirabelle_arith.ML
     Author:     Jasmin Blanchette, TU Munich
     Author:     Sascha Boehme, TU Munich
     Author:     Makarius

--- a/src/HOL/Tools/Mirabelle/mirabelle_metis.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Mirabelle/Tools/mirabelle_metis.ML
+(*  Title:      HOL/Tools/Mirabelle/mirabelle_metis.ML
     Author:     Jasmin Blanchette, TU Munich
     Author:     Sascha Boehme, TU Munich
     Author:     Martin Desharnais, UniBw Munich

--- a/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Mirabelle/Tools/mirabelle_presburger.ML
+(*  Title:      HOL/Tools/Mirabelle/mirabelle_presburger.ML
     Author:     Martin Desharnais, MPI-INF Saarbrücken
 
 Mirabelle action: "presburger".

--- a/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
+(*  Title:      HOL/Tools/Mirabelle/mirabelle_quickcheck.ML
     Author:     Jasmin Blanchette, TU Munich
     Author:     Sascha Boehme, TU Munich
     Author:     Martin Desharnais, UniBw Munich

--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
+(*  Title:      HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
     Author:     Jasmin Blanchette, TU Munich
     Author:     Sascha Boehme, TU Munich
     Author:     Tobias Nipkow, TU Munich

--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
+(*  Title:      HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML
     Author:     Jasmin Blanchette, TU Munich
     Author:     Makarius
     Author:     Martin Desharnais, UniBw Munich

--- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Mirabelle/Tools/mirabelle_try0.ML
+(*  Title:      HOL/Tools/Mirabelle/mirabelle_try0.ML
     Author:     Jasmin Blanchette, TU Munich
     Author:     Makarius
     Author:     Martin Desharnais, UniBw Munich

--- a/src/HOL/Tools/Mirabelle/mirabelle_util.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_util.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Mirabelle/Tools/mirabelle_util.ML
+(*  Title:      HOL/Tools/Mirabelle/mirabelle_util.ML
     Author:     Martin Desharnais, MPI-INF Saarbruecken
 *)
 

--- a/src/HOL/Tools/SMT/lethe_isar.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/SMT/lethe_isar.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/SMT/verit_isar.ML
+(*  Title:      HOL/Tools/SMT/lethe_isar.ML
     Author:     Mathias Fleury, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 

--- a/src/HOL/Tools/SMT/lethe_proof.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/SMT/lethe_proof.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/SMT/Lethe_Proof.ML
+(*  Title:      HOL/Tools/SMT/lethe_proof.ML
     Author:     Mathias Fleury, ENS Rennes
     Author:     Sascha Boehme, TU Muenchen
 

--- a/src/HOL/Tools/SMT/lethe_proof_parse.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/SMT/lethe_proof_parse.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/SMT/verit_proof_parse.ML
+(*  Title:      HOL/Tools/SMT/lethe_proof_parse.ML
     Author:     Mathias Fleury, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 

--- a/src/HOL/Tools/SMT/lethe_replay_methods.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/SMT/lethe_replay_methods.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/SMT/verit_replay_methods.ML
+(*  Title:      HOL/Tools/SMT/lethe_replay_methods.ML
     Author:     Mathias Fleury, MPII, JKU, University Freiburg
 
 Proof method for replaying veriT proofs.

--- a/src/HOL/Tools/SMT/verit_strategies.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/SMT/verit_strategies.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/SMT/Verit_Proof.ML
+(*  Title:      HOL/Tools/SMT/verit_strategies.ML
     Author:     Mathias Fleury, ENS Rennes, MPI, JKU, Freiburg University
 
 VeriT proofs: parsing and abstract syntax tree.

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/ATP/atp_systems.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
     Author:     Fabian Immler, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 

--- a/src/Provers/preorder.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/Provers/preorder.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      src/Provers/preorder.ML
+(*  Title:      Provers/preorder.ML
     Author:     Oliver Kutter, TU Muenchen
 
 Reasoner for simple transitivity and quasi orders.

--- a/src/Pure/Admin/build_cvc5.scala	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/Pure/Admin/build_cvc5.scala	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-/*  Title:      Pure/Admin/build_cvc5scala
+/*  Title:      Pure/Admin/build_cvc5.scala
     Author:     Makarius
 
 Build Isabelle component for cvc5. See also:

--- a/src/Pure/General/base64.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/Pure/General/base64.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/System/base64.ML
+(*  Title:      Pure/General/base64.ML
     Author:     Makarius
 
 Support for Base64 data encoding (via Isabelle/Scala).

--- a/src/Pure/General/xz.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/Pure/General/xz.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/System/xz.ML
+(*  Title:      Pure/General/xz.ML
     Author:     Makarius
 
 Support for XZ compression (via Isabelle/Scala).

--- a/src/Pure/PIDE/byte_message.ML	Sat Sep 17 16:16:38 2022 +0200
+++ b/src/Pure/PIDE/byte_message.ML	Sat Sep 17 16:50:39 2022 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/General/byte_message.ML
+(*  Title:      Pure/PIDE/byte_message.ML
     Author:     Makarius
 
 Byte-oriented messages.