src/HOL/UNITY/UNITY.ML

 
 
 (*** increasing ***)
 
 Goalw [increasing_def, stable_def, constrains_def]
-     "increasing f <= increasing (length o f)";
-by Auto_tac;
-by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
-qed "increasing_size";
+     "mono g ==> increasing f <= increasing (g o f)";
+by Auto_tac;
+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}}";
 by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
 by (Blast_tac 1);