equal
deleted
inserted
replaced
5 Conditional Fairness versions of transient, ensures, leadsTo. |
5 Conditional Fairness versions of transient, ensures, leadsTo. |
6 |
6 |
7 From Misra, "A Logic for Concurrent Programming", 1994 |
7 From Misra, "A Logic for Concurrent Programming", 1994 |
8 *) |
8 *) |
9 |
9 |
10 header{*Progress*} |
10 section{*Progress*} |
11 |
11 |
12 theory WFair imports UNITY begin |
12 theory WFair imports UNITY begin |
13 |
13 |
14 text{*The original version of this theory was based on weak fairness. (Thus, |
14 text{*The original version of this theory was based on weak fairness. (Thus, |
15 the entire UNITY development embodied this assumption, until February 2003.) |
15 the entire UNITY development embodied this assumption, until February 2003.) |