changeset 60770 | 240563fbf41d |
parent 58871 | c399ae4b836f |
child 61392 | 331be2820f90 |
60769:cf7f3465eaf1 | 60770:240563fbf41d |
---|---|
17 |
17 |
18 Theory ported from HOL. |
18 Theory ported from HOL. |
19 *) |
19 *) |
20 |
20 |
21 |
21 |
22 section{*The Chandy-Sanders Guarantees Operator*} |
22 section\<open>The Chandy-Sanders Guarantees Operator\<close> |
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???? *) |