--- a/src/ZF/Epsilon.ML Thu Oct 16 13:38:47 1997 +0200
+++ b/src/ZF/Epsilon.ML Thu Oct 16 13:39:20 1997 +0200
@@ -269,14 +269,6 @@
by (rtac (consI1 RS consI2 RS rank_lt) 1);
qed "rank_pair2";
-goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) < rank(Inl(a))";
-by (rtac rank_pair2 1);
-val rank_Inl = result();
-
-goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) < rank(Inr(a))";
-by (rtac rank_pair2 1);
-val rank_Inr = result();
-
(*** Corollaries of leastness ***)
goal Epsilon.thy "!!A B. A:B ==> eclose(A)<=eclose(B)";
--- a/src/ZF/Univ.ML Thu Oct 16 13:38:47 1997 +0200
+++ b/src/ZF/Univ.ML Thu Oct 16 13:39:20 1997 +0200
@@ -470,6 +470,14 @@
(** Set up an environment for simplification **)
+goalw Univ.thy [Inl_def] "rank(a) < rank(Inl(a))";
+by (rtac rank_pair2 1);
+qed "rank_Inl";
+
+goalw Univ.thy [Inr_def] "rank(a) < rank(Inr(a))";
+by (rtac rank_pair2 1);
+qed "rank_Inr";
+
val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2];
val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans]));