--- a/src/ZF/UNITY/Increasing.ML Fri Jun 27 13:15:40 2003 +0200
+++ b/src/ZF/UNITY/Increasing.ML Fri Jun 27 18:40:25 2003 +0200
@@ -37,7 +37,7 @@
Addsimps [increasing_constant];
Goalw [increasing_def, stable_def, part_order_def,
- constrains_def, mono1_def, comp_def]
+ constrains_def, mono1_def, metacomp_def]
"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> \
\ increasing[A](r, f) <= increasing[B](s, g comp f)";
by (Clarify_tac 1);
@@ -113,7 +113,7 @@
Addsimps [Increasing_constant];
Goalw [Increasing_def, Stable_def, Constrains_def, part_order_def,
- constrains_def, mono1_def, comp_def]
+ constrains_def, mono1_def, metacomp_def]
"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> \
\ Increasing[A](r, f) <= Increasing[B](s, g comp f)";
by Safe_tac;