src/HOL/UNITY/UNITY.ML

 Goalw [increasing_def]
      "F : increasing f ==> F : stable {s. z <= f s}";
 by (Blast_tac 1);
 qed "increasingD";
 
+Goalw [increasing_def, stable_def] "F : increasing (%s. c)";
+by Auto_tac; 
+qed "increasing_constant";
+AddIffs [increasing_constant];
+
 Goalw [increasing_def, stable_def, constrains_def]
      "mono g ==> increasing f <= increasing (g o f)";
 by Auto_tac;
 by (blast_tac (claset() addIs [monoD, order_trans]) 1);
 qed "mono_increasing_o";