--- 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 ***
--- 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
--- 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
--- 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 =