# HG changeset patch
# User wenzelm
# Date 877001960 -7200
# Node ID 59bab7a52b4c1d2252b2ebbd37d40a59fde83e86
# Parent  85eb8e24c5ffceb9f0ca44b4d52a146aa83a06a6
moved rank_Inl, rank_Inr from Epsilon.ML to Univ.ML;

diff -r 85eb8e24c5ff -r 59bab7a52b4c src/ZF/Epsilon.ML
--- 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)";
diff -r 85eb8e24c5ff -r 59bab7a52b4c src/ZF/Univ.ML
--- 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]));