# HG changeset patch
# User lcp
# Date 789876125 -3600
# Node ID a4b286dfdd6f1830e18b714fc2cb667b4028835b
# Parent  664052e3cf66ede02e05479f72cb69760d4b0583
Moved theorems Ord_cases_lemma and Ord_cases to Ordinal.ML

diff -r 664052e3cf66 -r a4b286dfdd6f src/ZF/Univ.ML
--- a/src/ZF/Univ.ML	Thu Jan 12 03:01:40 1995 +0100
+++ b/src/ZF/Univ.ML	Thu Jan 12 03:02:05 1995 +0100
@@ -163,21 +163,6 @@
 by (fast_tac ZF_cs 1);
 qed "Vfrom_Union";
 
-goal Univ.thy "!!i. Ord(i) ==> i=0 | (EX j. i=succ(j)) | Limit(i)";
-by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_lt]) 1);
-qed "Ord_cases_lemma";
-
-val major::prems = goal Univ.thy
-    "[| Ord(i);			\
-\       i=0            ==> P;	\
-\       !!j. i=succ(j) ==> P;	\
-\       Limit(i)       ==> P	\
-\    |] ==> P";
-by (cut_facts_tac [major RS Ord_cases_lemma] 1);
-by (REPEAT (eresolve_tac (prems@[disjE, exE]) 1));
-qed "Ord_cases";
-
-
 (*** Vfrom applied to Limit ordinals ***)
 
 (*NB. limit ordinals are non-empty;