# HG changeset patch
# User paulson
# Date 858678128 -3600
# Node ID f119c3686782cfe54f4a448f69013fb78ad6b91f
# Parent  56948cb1a1f912a84685e2458e58e0b3b6505371
Stopped giving Introduction rules as Elimination rules

diff -r 56948cb1a1f9 -r f119c3686782 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Tue Mar 18 08:43:26 1997 +0100
+++ b/src/ZF/Cardinal.ML	Tue Mar 18 10:42:08 1997 +0100
@@ -147,7 +147,7 @@
 
 goalw Cardinal.thy [lepoll_def]
         "!!A. [| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)";
-by (fast_tac (!claset addSEs [well_ord_rvimage]) 1);
+by (fast_tac (!claset addIs [well_ord_rvimage]) 1);
 qed "lepoll_well_ord";
 
 goalw Cardinal.thy [lesspoll_def] "A lepoll B <-> A lesspoll B | A eqpoll B";
@@ -282,7 +282,7 @@
 
 goal Cardinal.thy
     "!!X Y. [| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| <-> X eqpoll Y";
-by (fast_tac (!claset addSEs [cardinal_cong, well_ord_cardinal_eqE]) 1);
+by (fast_tac (!claset addIs [cardinal_cong, well_ord_cardinal_eqE]) 1);
 qed "well_ord_cardinal_eqpoll_iff";
 
 
@@ -393,7 +393,7 @@
 qed "Card_lt_imp_lt";
 
 goal Cardinal.thy "!!i j. [| Ord(i);  Card(K) |] ==> (|i| < K) <-> (i < K)";
-by (fast_tac (!claset addEs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1);
+by (fast_tac (!claset addIs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1);
 qed "Card_lt_iff";
 
 goal Cardinal.thy "!!i j. [| Ord(i);  Card(K) |] ==> (K le |i|) <-> (K le i)";