src/HOL/UNITY/Constrains.thy

     "Unless A B == Constrains (A-B) (A Un B)"
 
   Invariant :: "'a set => 'a program set"
     "Invariant A == {F. Init F <= A} Int Stable A"
 
+  (*Polymorphic in both states and the meaning of <= *)
+  Increasing :: "['a => 'b::{ord}] => 'a program set"
+    "Increasing f == INT z. Stable {s. z <= f s}"
+
 end