src/HOL/UNITY/WFair.thy
changeset 10834 a7897aebbffc
parent 10797 028d22926a41
child 13797 baefae13ad37
--- a/src/HOL/UNITY/WFair.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/WFair.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -15,7 +15,7 @@
   (*This definition specifies weak fairness.  The rest of the theory
     is generic to all forms of fairness.*)
   transient :: "'a set => 'a program set"
-    "transient A == {F. EX act: Acts F. A <= Domain act & act```A <= -A}"
+    "transient A == {F. EX act: Acts F. A <= Domain act & act``A <= -A}"
 
   ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
     "A ensures B == (A-B co A Un B) Int transient (A-B)"