equal
deleted
inserted
replaced
13 constdefs |
13 constdefs |
14 |
14 |
15 (*This definition specifies weak fairness. The rest of the theory |
15 (*This definition specifies weak fairness. The rest of the theory |
16 is generic to all forms of fairness.*) |
16 is generic to all forms of fairness.*) |
17 transient :: "'a set => 'a program set" |
17 transient :: "'a set => 'a program set" |
18 "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= Compl A}" |
18 "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}" |
19 |
19 |
20 ensures :: "['a set, 'a set] => 'a program set" |
20 ensures :: "['a set, 'a set] => 'a program set" |
21 "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)" |
21 "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)" |
22 |
22 |
23 |
23 |