Fix a numeral/exp simplification to only fire on numerals

HOL-Theorem-Prover · Jun 1, 2023 · 318e93f · 318e93f
1 parent 990630a
commit 318e93f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/num/extra_theories/logrootScript.sml b/src/num/extra_theories/logrootScript.sml
@@ -338,7 +338,7 @@ fun conj3 (x,y,z) = CONJ x (CONJ y z)
 
 Theorem LE_EXP_LOG_SIMP[simp] =
         LT_EXP_LOG
-        |> Q.INST [‘x’ |-> ‘x - 1’]
+        |> Q.INST [‘x’ |-> ‘x - 1’, ‘b’ |-> ‘NUMERAL b’]
         |> SIMP_RULE bool_ss
                      [DECIDE “0 < x ==> (x - 1 < y <=> x <= y)”, ASSUME “0 < x”]
         |> DISCH_ALL