# 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.