equal
deleted
inserted
replaced
20 |
20 |
21 strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set" |
21 strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set" |
22 "strongest_rhs Acts A == Inter {B. constrains Acts A B}" |
22 "strongest_rhs Acts A == Inter {B. constrains Acts A B}" |
23 |
23 |
24 unless :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
24 unless :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
25 "unless mutex A B == constrains mutex (A-B) (A Un B)" |
25 "unless Acts A B == constrains Acts (A-B) (A Un B)" |
26 |
26 |
27 end |
27 end |