# HG changeset patch
# User paulson
# Date 959963438 -7200
# Node ID e50c0764e522445571f2043d97b454bb89d0e737
# Parent  b1f37f6819c42a4cafaf70861f18c5c17e43205a
new theorem increasing_constant

diff -r b1f37f6819c4 -r e50c0764e522 src/HOL/UNITY/UNITY.ML
--- 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;