equal
deleted
inserted
replaced
49 (*Always is the weak form of "invariant"*) |
49 (*Always is the weak form of "invariant"*) |
50 Always :: "'a set => 'a program set" |
50 Always :: "'a set => 'a program set" |
51 "Always A == {F. Init F <= A} Int Stable A" |
51 "Always A == {F. Init F <= A} Int Stable A" |
52 |
52 |
53 (*Polymorphic in both states and the meaning of <= *) |
53 (*Polymorphic in both states and the meaning of <= *) |
54 Increasing :: "['a => 'b::{ord}] => 'a program set" |
54 Increasing :: "['a => 'b::{order}] => 'a program set" |
55 "Increasing f == INT z. Stable {s. z <= f s}" |
55 "Increasing f == INT z. Stable {s. z <= f s}" |
56 |
56 |
57 end |
57 end |