Got rid of last pesky unicode

HOL-Theorem-Prover · Jul 29, 2019 · 2bc2f0b · 2bc2f0b
1 parent 79a8799
commit 2bc2f0b
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/relation/relationScript.sml b/src/relation/relationScript.sml
@@ -2296,10 +2296,10 @@ val Newmans_lemma = store_thm(
 
 val BISIM_def = new_definition(
   "BISIM_def",
-  ``BISIM ts R = !p q α.
+  ``BISIM ts R = !p q l.
                     R p q ==>
-                    (!p'. ts p α p' ==> (?q'. ts q α q' /\ R p' q')) /\
-                    (!q'. ts q α q' ==> (?p'. ts p α p' /\ R p' q'))``)
+                    (!p'. ts p l p' ==> (?q'. ts q l q' /\ R p' q')) /\
+                    (!q'. ts q l q' ==> (?p'. ts p l p' /\ R p' q'))``)
 
 val BISIM_REL_def = new_definition(
   "BISIM_REL_def",