new theorem increasing_constant

--- a/src/HOL/UNITY/UNITY.ML	Fri Jun 02 17:48:17 2000 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Fri Jun 02 18:30:38 2000 +0200
@@ -300,6 +300,11 @@
 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;