# HG changeset patch
# User paulson
# Date 927553823 -7200
# Node ID d1bebb7f1c50e60a96e9e3e55ffc0d28ea4cf052
# Parent  d45359e7dcbf137a86862615c163c77482a8e7e7
generalized increasing_size to mono_increasing_o

diff -r d45359e7dcbf -r d1bebb7f1c50 src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Mon May 24 15:49:44 1999 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Mon May 24 15:50:23 1999 +0200
@@ -266,10 +266,10 @@
 (*** increasing ***)
 
 Goalw [increasing_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}}";