# HG changeset patch
# User paulson
# Date 927553554 -7200
# Node ID 5febcf428342707f8f0f5a7f4b6a8f4614082a0f
# Parent  8103c1fb092d195961b99c76d8a82fb32ebd3187
generalized Increasing_size to mono_Increasing_o

diff -r 8103c1fb092d -r 5febcf428342 src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Mon May 24 15:45:22 1999 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Mon May 24 15:45:54 1999 +0200
@@ -201,10 +201,10 @@
 (*** Increasing ***)
 
 Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
-     "Increasing f <= Increasing (length o f)";
+     "mono g ==> Increasing f <= Increasing (g o f)";
 by Auto_tac;
-by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
-qed "Increasing_size";
+by (blast_tac (claset() addIs [monoD, order_trans]) 1);
+qed "mono_Increasing_o";
 
 Goalw [Increasing_def]
      "Increasing f <= {F. ALL z::nat. F: Stable {s. z < f s}}";
@@ -218,7 +218,6 @@
 qed "increasing_imp_Increasing";
 
 
-
 (*** The Elimination Theorem.  The "free" m has become universally quantified!
      Should the premise be !!m instead of ALL m ?  Would make it harder to use
      in forward proof. ***)