Remove some unicode

HOL-Theorem-Prover · Jun 18, 2024 · 493fc3f · 493fc3f
1 parent 8ec5529
commit 493fc3f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/num/theories/cv_compute/automation/cv_stdScript.sml b/src/num/theories/cv_compute/automation/cv_stdScript.sml
@@ -274,7 +274,7 @@ val res = cv_trans count_loop_def;
 Theorem cv_COUNT_LIST[cv_inline]:
   COUNT_LIST n = count_loop n 0
 Proof
-  qsuff_tac `∀n k. count_loop n k = MAP (λi. i + k) (COUNT_LIST n)` >>
+  qsuff_tac `!n k. count_loop n k = MAP (\i. i + k) (COUNT_LIST n)` >>
   simp[] >>
   Induct \\ rw[] \\ simp [rich_listTheory.COUNT_LIST_def,Once count_loop_def]
   \\ gvs [MAP_MAP_o,combinTheory.o_DEF,ADD1] \\ AP_THM_TAC \\ AP_TERM_TAC