src/HOL/UNITY/Constrains.ML
changeset 6704 5febcf428342
parent 6672 8542c6dda828
child 6739 66e4118eead9
--- 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. ***)