HolSmt: add let, ediv and emod simps to thm_AUTO

HOL-Theorem-Prover · Mar 14, 2024 · 4047092 · 4047092
1 parent e14320c
commit 4047092
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
@@ -107,7 +107,8 @@ fun auto_tac (_, t) =
     val simpset = bossLib.++ (bossLib.srw_ss (), wordsLib.WORD_ss)
     val t_eq_t' = simpLib.SIMP_CONV simpset [integerTheory.INT_ABS,
       integerTheory.INT_MAX, integerTheory.INT_MIN, integerTheory.int_quot,
-      integerTheory.int_rem]
+      integerTheory.int_rem, integerTheory.EDIV_DEF, integerTheory.EMOD_DEF,
+      boolTheory.LET_THM]
       t
       handle Conv.UNCHANGED =>
         Thm.REFL t