Fix Unicode violation

HOL-Theorem-Prover · Sep 11, 2023 · 11636cd · 11636cd
1 parent 0692807
commit 11636cd
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/transfer/examples/fmspScript.sml b/src/transfer/examples/fmspScript.sml
@@ -179,7 +179,7 @@ Definition sp2fm_def:
 End
 
 Theorem sp2fm_correct:
-  FMSP (=) (=) fm sp ⇔ wf sp /\ fm = sp2fm sp
+  FMSP (=) (=) fm sp <=> wf sp /\ fm = sp2fm sp
 Proof
   simp[FMSP_def, sp2fm_def, EQ_IMP_THM, FLOOKUP_SIMP, AllCaseEqs()] >>
   rpt conj_tac