--- 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. ***)