Fix/simplify proof broken by recent HOL change

CakeML · Jul 5, 2022 · 4745ef9 · 4745ef9
1 parent cbf165f
commit 4745ef9
Showing 1 changed file with 3 additions and 6 deletions.
diff --git a/basis/pure/mlintScript.sml b/basis/pure/mlintScript.sml
@@ -372,12 +372,9 @@ Proof
   \\ qspec_then`Num n`assume_tac EVERY_isDigit_num_to_dec_string
   \\ Cases_on`num_to_dec_string (Num n)` \\ fs[]
   \\ rw[]
-  \\ TRY ( qhdtm_x_assum`isDigit`mp_tac \\ EVAL_TAC \\ NO_TAC )
-  \\ mp_tac ASCIInumbersTheory.num_dec_string
-  \\ simp[FUN_EQ_THM]
-  \\ disch_then(qspec_then`Num n`mp_tac)
-  \\ simp[]
-  \\ simp[integerTheory.INT_OF_NUM]
+  \\ gs[stringTheory.isDigit_def]
+  \\ qpat_x_assum ‘toString _ = _’ (SUBST1_TAC o SYM)
+  \\ simp[toNum_toString, integerTheory.INT_OF_NUM]
 QED
 
 Triviality fromString_helper: