src/HOL/SMT.thy
changeset 75956 1e2a9d2251b0
parent 75936 d2e6a1342c90
child 76106 98cab94326d4
--- a/src/HOL/SMT.thy	Sun Aug 21 14:01:59 2022 +0000
+++ b/src/HOL/SMT.thy	Mon Aug 22 06:27:28 2022 +0200
@@ -627,7 +627,6 @@
 ML_file \<open>Tools/SMT/lethe_isar.ML\<close>
 ML_file \<open>Tools/SMT/lethe_proof_parse.ML\<close>
 ML_file \<open>Tools/SMT/cvc_proof_parse.ML\<close>
-ML_file \<open>Tools/SMT/verit_proof.ML\<close>
 ML_file \<open>Tools/SMT/conj_disj_perm.ML\<close>
 ML_file \<open>Tools/SMT/smt_replay_methods.ML\<close>
 ML_file \<open>Tools/SMT/smt_replay.ML\<close>
@@ -638,6 +637,7 @@
 ML_file \<open>Tools/SMT/z3_replay.ML\<close>
 ML_file \<open>Tools/SMT/lethe_replay_methods.ML\<close>
 ML_file \<open>Tools/SMT/verit_replay_methods.ML\<close>
+ML_file \<open>Tools/SMT/verit_strategies.ML\<close>
 ML_file \<open>Tools/SMT/verit_replay.ML\<close>
 ML_file \<open>Tools/SMT/smt_systems.ML\<close>