# HG changeset patch
# User lcp
# Date 797766007 -7200
# Node ID 03063caa960a6ec0b3c88dc7caaf2a8e120c2957
# Parent  0d28f4bc8a446ffa64a5063e4a84d5d90eb5277a
Deleted lt_oadd_disj1

diff -r 0d28f4bc8a44 -r 03063caa960a src/ZF/AC/AC_Equiv.ML
--- a/src/ZF/AC/AC_Equiv.ML	Thu Apr 13 11:38:48 1995 +0200
+++ b/src/ZF/AC/AC_Equiv.ML	Thu Apr 13 11:40:07 1995 +0200
@@ -97,16 +97,6 @@
 by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1);
 val ordertype_Int = result();
 
-(* used only in WO6WO1.ML *)
-(* corrected according to LCP'a advise *)
-goal Cardinal.thy 
-      "!!i j k. [| k < i++j; Ord(i); Ord(j) |] ==>  \
-\                  k<i | (EX! l. l<j & k = i++l)";
-by (dresolve_tac [lt_oadd_disj] 1 THEN (REPEAT (atac 1)));
-by (fast_tac (ZF_cs addIs [ex1I, ltI] addSEs [oadd_inject RS sym, lt_Ord]
-		addEs [Ord_in_Ord]) 1);
-val lt_oadd_disj1 = result();
-
 (* used only in AC16_lemmas.ML *)
 goalw CardinalArith.thy [InfCard_def]
 	"!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)";