# HG changeset patch
# User Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1602600338 -7200
# Node ID 15fc6320da6807a5f29ba853a71ab3ac637e060f
# Parent  b44e894796d5160642338720642d94768908a274
reconstruction of veriT proofs in NEWS

diff -r b44e894796d5 -r 15fc6320da68 NEWS
--- a/NEWS	Mon Oct 12 18:59:44 2020 +0200
+++ b/NEWS	Tue Oct 13 16:45:38 2020 +0200
@@ -159,7 +159,8 @@
 all problems.
 
 * SMT reconstruction: It is now possible to reconstruct proofs from the
-SMT solver veriT via the tactic veriT_smt.
+SMT solver veriT by calling "smt (verit)".
+
 
 *** FOL ***
 
diff -r b44e894796d5 -r 15fc6320da68 src/HOL/Tools/SMT/verit_isar.ML
--- a/src/HOL/Tools/SMT/verit_isar.ML	Mon Oct 12 18:59:44 2020 +0200
+++ b/src/HOL/Tools/SMT/verit_isar.ML	Tue Oct 13 16:45:38 2020 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/SMT/lethe_isar.ML
+(*  Title:      HOL/Tools/SMT/verit_isar.ML
     Author:     Mathias Fleury, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 
diff -r b44e894796d5 -r 15fc6320da68 src/HOL/Tools/SMT/verit_replay.ML
--- a/src/HOL/Tools/SMT/verit_replay.ML	Mon Oct 12 18:59:44 2020 +0200
+++ b/src/HOL/Tools/SMT/verit_replay.ML	Tue Oct 13 16:45:38 2020 +0200
@@ -137,10 +137,10 @@
     val args = map (Term.subst_free concl_tranformation o subst_only_free global_transformation) args
     val insts = Symtab.map (K (Term.subst_free concl_tranformation o subst_only_free global_transformation)) insts
     val proof_prems =
-       if Lethe_Replay_Methods.requires_subproof_assms prems rule then proof_prems else []
+       if Verit_Replay_Methods.requires_subproof_assms prems rule then proof_prems else []
     val local_inputs =
-       if Lethe_Replay_Methods.requires_local_input prems rule then input @ inputs else []
-    val replay = Timing.timing (replay_thm Lethe_Replay_Methods.method_for rewrite_rules ll_defs
+       if Verit_Replay_Methods.requires_local_input prems rule then input @ inputs else []
+    val replay = Timing.timing (replay_thm Verit_Replay_Methods.method_for rewrite_rules ll_defs
        ctxt assumed [] (proof_prems @ local_inputs) (nthms @ nthms') concl_tranformation
        global_transformation args insts)
 
@@ -313,7 +313,7 @@
     val _ = SMT_Replay.spying (SMT_Config.spy_verit ctxt) ctxt
       (fn () => SMT_Replay.print_stats (Symtab.dest stats)) "spy_verit"
   in
-    Lethe_Replay_Methods.discharge ctxt [thm_with_defs] @{term False}
+    Verit_Replay_Methods.discharge ctxt [thm_with_defs] @{term False}
   end
 
 end
diff -r b44e894796d5 -r 15fc6320da68 src/HOL/Tools/SMT/verit_replay_methods.ML
--- a/src/HOL/Tools/SMT/verit_replay_methods.ML	Mon Oct 12 18:59:44 2020 +0200
+++ b/src/HOL/Tools/SMT/verit_replay_methods.ML	Tue Oct 13 16:45:38 2020 +0200
@@ -4,7 +4,7 @@
 Proof method for replaying veriT proofs.
 *)
 
-signature LETHE_REPLAY_METHODS =
+signature VERIT_REPLAY_METHODS =
 sig
   (*methods for verit proof rules*)
   val method_for: string -> Proof.context -> thm list -> term list -> term Symtab.table ->
@@ -17,7 +17,7 @@
 end;
 
 
-structure Lethe_Replay_Methods: LETHE_REPLAY_METHODS =
+structure Verit_Replay_Methods: VERIT_REPLAY_METHODS =
 struct
 
 (*Some general comments on the proof format:
@@ -1163,7 +1163,7 @@
   | choose Trans = ignore_args trans
   | choose r = unsupported (string_of_verit_rule r)
 
-type Lethe_method = Proof.context -> thm list -> term -> thm
+type verit_method = Proof.context -> thm list -> term -> thm
 type abs_context = int * term Termtab.table
 
 fun with_tracing rule method ctxt thms args insts decls t =