| changeset 58871 | c399ae4b836f |
| parent 46823 | 57bf0cecb366 |
| child 60770 | 240563fbf41d |
| 58870:e2c0d8ef29cb | 58871:c399ae4b836f |
|---|---|
17 |
17 |
18 Theory ported from HOL. |
18 Theory ported from HOL. |
19 *) |
19 *) |
20 |
20 |
21 |
21 |
22 header{*The Chandy-Sanders Guarantees Operator*} |
22 section{*The Chandy-Sanders Guarantees Operator*} |
23 |
23 |
24 theory Guar imports Comp begin |
24 theory Guar imports Comp begin |
25 |
25 |
26 |
26 |
27 (* To be moved to theory WFair???? *) |
27 (* To be moved to theory WFair???? *) |