Fix Unicode violation

HOL-Theorem-Prover · Dec 2, 2023 · 8f60f1f · 8f60f1f
1 parent 0bbc579
commit 8f60f1f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml
@@ -348,7 +348,7 @@ val MAP_FOLDL = Q.store_thm ("MAP_FOLDL",
 Theorem FOLDL_CONG_invariant:
   !P f1 f2 l e.
   P e /\
-  (!x a. MEM x l ∧ P a ==> f1 a x = f2 a x /\ P (f2 a x))
+  (!x a. MEM x l /\ P a ==> f1 a x = f2 a x /\ P (f2 a x))
   ==>
   FOLDL f1 e l = FOLDL f2 e l /\ P (FOLDL f2 e l)
 Proof