Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/SMT/verit_replay_methods.ML
changeset 78177 ea7a3cc64df5
parent 75561 b6239ed66b94 
--- a/src/HOL/Tools/SMT/verit_replay_methods.ML	Sat Jun 17 17:41:02 2023 +0200
+++ b/src/HOL/Tools/SMT/verit_replay_methods.ML	Mon Jun 19 22:28:09 2023 +0200
@@ -120,7 +120,7 @@
   | choose Bind = ignore_insts bind
   | choose Bool_Simplify = ignore_args rewrite_bool_simplify
   | choose Comp_Simplify = ignore_args rewrite_comp_simplify
-  | choose Cong = ignore_args cong
+  | choose Cong = ignore_args (cong "verit")
   | choose Connective_Def = ignore_args rewrite_connective_def
   | choose Duplicate_Literals = ignore_args duplicate_literals
   | choose Eq_Congruent = ignore_args eq_congruent
@@ -156,7 +156,7 @@
   | choose LA_Tautology = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow
   | choose LA_Totality = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow
   | choose LIA_Generic = ignore_args lia_generic
-  | choose Local_Input = ignore_args refl
+  | choose Local_Input = ignore_args (refl "verit")
   | choose Minus_Simplify = ignore_args rewrite_minus_simplify
   | choose NLA_Generic = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow
   | choose Normalized_Input = ignore_args normalized_input
@@ -180,7 +180,7 @@
   | choose Qnt_Rm_Unused = ignore_args qnt_rm_unused
   | choose Onepoint = ignore_args onepoint
   | choose Qnt_Simplify = ignore_args qnt_simplify
-  | choose Refl = ignore_args refl
+  | choose Refl = ignore_args (refl "verit")
   | choose Resolution = ignore_args unit_res
   | choose Skolem_Ex = ignore_args skolem_ex
   | choose Skolem_Forall = ignore_args skolem_forall
isabelle