equal
deleted
inserted
replaced
8 From Misra, "A Logic for Concurrent Programming", 1994 |
8 From Misra, "A Logic for Concurrent Programming", 1994 |
9 |
9 |
10 Theory ported from HOL. |
10 Theory ported from HOL. |
11 *) |
11 *) |
12 |
12 |
13 WFair = UNITY + |
13 WFair = UNITY + Main_ZFC + |
14 constdefs |
14 constdefs |
15 |
15 |
16 (* This definition specifies weak fairness. The rest of the theory |
16 (* This definition specifies weak fairness. The rest of the theory |
17 is generic to all forms of fairness.*) |
17 is generic to all forms of fairness.*) |
18 transient :: "i=>i" |
18 transient :: "i=>i" |