Remove some Unicode

HOL-Theorem-Prover · Oct 19, 2024 · 76556b8 · 76556b8
1 parent 6caeaf9
commit 76556b8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/n-bit/wordsScript.sml b/src/n-bit/wordsScript.sml
@@ -4964,7 +4964,7 @@ Proof
   \\ Cases_on`dimword(:'a) = 2`
   >- (
     gs[word_mod_def, word_div_def]
-    \\ `w2n b < 2 ∧ w2n e < 2` by metis_tac[w2n_lt]
+    \\ `w2n b < 2 /\ w2n e < 2` by metis_tac[w2n_lt]
     \\ gs[NUMERAL_LESS_THM]
     \\ Cases_on`b` \\ gs[word_mul_n2w] )
   \\ `2 < dimword(:'a)`