From 76556b8cbba47889a465def07581c846a7edf789 Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Sat, 19 Oct 2024 23:16:01 +0100 Subject: [PATCH] Remove some Unicode --- src/n-bit/wordsScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/n-bit/wordsScript.sml b/src/n-bit/wordsScript.sml index 0f73819b49..007ac8b1c5 100644 --- 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)`