equal
deleted
inserted
replaced
49 increasing :: "['a => 'b::{order}] => 'a program set" |
49 increasing :: "['a => 'b::{order}] => 'a program set" |
50 "increasing f == INT z. stable {s. z <= f s}" |
50 "increasing f == INT z. stable {s. z <= f s}" |
51 |
51 |
52 |
52 |
53 defs |
53 defs |
54 constrains_def "A co B == {F. ALL act: Acts F. act```A <= B}" |
54 constrains_def "A co B == {F. ALL act: Acts F. act``A <= B}" |
55 |
55 |
56 unless_def "A unless B == (A-B) co (A Un B)" |
56 unless_def "A unless B == (A-B) co (A Un B)" |
57 |
57 |
58 end |
58 end |