--- a/src/HOL/UNITY/WFair.thy Wed Nov 18 11:12:29 1998 +0100
+++ b/src/HOL/UNITY/WFair.thy Wed Nov 18 15:10:46 1998 +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 <= Compl A}"
+ "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
ensures :: "['a set, 'a set] => 'a program set"
"ensures A B == constrains (A-B) (A Un B) Int transient (A-B)"