HolSmt: remove duplicate self-tests

These test cases are already being tested above in the `num` section.
HOL-Theorem-Prover · Jan 26, 2024 · 6aba5bc · 6aba5bc
1 parent 3e17105
commit 6aba5bc
Showing 1 changed file with 0 additions and 5 deletions.
diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
@@ -548,11 +548,6 @@ in
     (``(x:real) < x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:real) < y ==> 42 * x < 42 * y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
-    (``0n <= 1n``, [thm_AUTO, thm_YO]),
-    (``1n <= 0n``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
-    (``(x:num) <= x``, [thm_AUTO, thm_YO]),
-    (``(x:num) <= y ==> 2 * x <= 2 * y``, [thm_AUTO, thm_YO]),
-
     (``1r > 0r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``0r > 1r``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:real) > x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),