# HG changeset patch
# User lcp
# Date 787488653 -3600
# Node ID 5d2a7634da46f1c97e2df4c917a33f96cae334bd
# Parent  354a56e923ffaac770f1f2f25bc4f93124f5bf29
case_ss: now built upon ZF/Order/bij_inverse_ss.  Deleted
own bij_inverse_ss and replaces uses by case_ss

diff -r 354a56e923ff -r 5d2a7634da46 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Thu Dec 15 11:17:49 1994 +0100
+++ b/src/ZF/Cardinal.ML	Thu Dec 15 11:50:53 1994 +0100
@@ -406,14 +406,9 @@
 (*** Towards Cardinal Arithmetic ***)
 (** Congruence laws for successor, cardinal addition and multiplication **)
 
-val case_ss = ZF_ss addsimps [Inl_iff, Inl_Inr_iff, Inr_iff, Inr_Inl_iff,
-			      case_Inl, case_Inr, InlI, InrI];
-
-val bij_inverse_ss =
-    case_ss addsimps [bij_is_fun RS apply_type,
-		      bij_converse_bij RS bij_is_fun RS apply_type,
-		      left_inverse_bij, right_inverse_bij];
-
+val case_ss = 
+    bij_inverse_ss addsimps [Inl_iff, Inl_Inr_iff, Inr_iff, Inr_Inl_iff,
+			     case_Inl, case_Inr, InlI, InrI];
 
 (*Congruence law for  cons  under equipollence*)
 goalw Cardinal.thy [lepoll_def]
@@ -448,7 +443,7 @@
 	 ("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(fa)`y))")] 
     lam_bijective 1);
 by (safe_tac (ZF_cs addSEs [sumE]));
-by (ALLGOALS (asm_simp_tac bij_inverse_ss));
+by (ALLGOALS (asm_simp_tac case_ss));
 qed "sum_eqpoll_cong";
 
 (*Congruence law for * under equipollence*)
@@ -460,7 +455,7 @@
 		  ("d", "split(%x y. <converse(f)`x, converse(fa)`y>)")] 
     lam_bijective 1);
 by (safe_tac ZF_cs);
-by (ALLGOALS (asm_simp_tac bij_inverse_ss));
+by (ALLGOALS (asm_simp_tac case_ss));
 qed "prod_eqpoll_cong";
 
 goalw Cardinal.thy [eqpoll_def]