# HG changeset patch
# User wenzelm
# Date 1663426239 -7200
# Node ID 8089593a364a3af828b2b513ad9f5056a0cbd22a
# Parent  11fed9812b57c84e5ebfd46c6ec8c11f8a2f8742
proper file headers;

diff -r 11fed9812b57 -r 8089593a364a src/HOL/Library/Sum_of_Squares/positivstellensatz.ML
--- 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
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Library/Tools/smt_word.ML
--- 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.
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Library/Tools/word_lib.ML
--- 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.
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/Mirabelle/mirabelle.ML
--- 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
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/Mirabelle/mirabelle_arith.ML
--- 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
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/Mirabelle/mirabelle_metis.ML
--- 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
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/Mirabelle/mirabelle_presburger.ML
--- 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".
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML
--- 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
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- 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
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML
--- 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
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/Mirabelle/mirabelle_try0.ML
--- 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
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/Mirabelle/mirabelle_util.ML
--- 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
 *)
 
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/SMT/lethe_isar.ML
--- 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
 
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/SMT/lethe_proof.ML
--- 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
 
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/SMT/lethe_proof_parse.ML
--- 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
 
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/SMT/lethe_replay_methods.ML
--- 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.
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/SMT/verit_strategies.ML
--- 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.
diff -r 11fed9812b57 -r 8089593a364a src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- 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
 
diff -r 11fed9812b57 -r 8089593a364a src/Provers/preorder.ML
--- 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.
diff -r 11fed9812b57 -r 8089593a364a src/Pure/Admin/build_cvc5.scala
--- 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:
diff -r 11fed9812b57 -r 8089593a364a src/Pure/General/base64.ML
--- 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).
diff -r 11fed9812b57 -r 8089593a364a src/Pure/General/xz.ML
--- 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).
diff -r 11fed9812b57 -r 8089593a364a src/Pure/PIDE/byte_message.ML
--- 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.