tidied some proofs
authorpaulson
Mon Feb 07 15:14:02 2000 +0100 (2000-02-07)
changeset 8201a81d18b0a9b1
parent 8200 700067a98634
child 8202 f32931b93686
tidied some proofs
src/ZF/Arith.ML
src/ZF/CardinalArith.ML
src/ZF/Epsilon.ML
src/ZF/Finite.ML
src/ZF/Integ/Int.ML
src/ZF/Order.ML
src/ZF/OrderArith.ML
src/ZF/Resid/Substitution.ML
src/ZF/Sum.ML
src/ZF/ex/Limit.ML
src/ZF/ex/Primrec.ML
src/ZF/func.ML
     1.1 --- a/src/ZF/Arith.ML	Sat Feb 05 17:31:53 2000 +0100
     1.2 +++ b/src/ZF/Arith.ML	Mon Feb 07 15:14:02 2000 +0100
     1.3 @@ -78,8 +78,7 @@
     1.4      "[| m:nat;  n:nat |] ==> m #- n le m";
     1.5  by (rtac (prems MRS diff_induct) 1);
     1.6  by (etac leE 3);
     1.7 -by (ALLGOALS
     1.8 -    (asm_simp_tac (simpset() addsimps prems @ [le_iff, nat_into_Ord])));
     1.9 +by (ALLGOALS (asm_simp_tac (simpset() addsimps prems @ [le_iff])));
    1.10  qed "diff_le_self";
    1.11  
    1.12  (*** Simplification over add, mult, diff ***)
    1.13 @@ -284,7 +283,7 @@
    1.14      [Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
    1.15       nat_into_Ord, not_lt_iff_le RS iffD1];
    1.16  
    1.17 -val div_ss = simpset() addsimps [nat_into_Ord, div_termination RS ltD,
    1.18 +val div_ss = simpset() addsimps [div_termination RS ltD,
    1.19  				 not_lt_iff_le RS iffD2];
    1.20  
    1.21  (*Type checking depends upon termination!*)
    1.22 @@ -336,7 +335,7 @@
    1.23  by (Asm_simp_tac 2);
    1.24  (*case n le x*)
    1.25  by (asm_full_simp_tac
    1.26 -     (simpset() addsimps [not_lt_iff_le, nat_into_Ord, add_assoc,
    1.27 +     (simpset() addsimps [not_lt_iff_le, add_assoc,
    1.28                           div_termination RS ltD, add_diff_inverse]) 1);
    1.29  qed "mod_div_equality";
    1.30  
    1.31 @@ -352,8 +351,7 @@
    1.32  				      succ_neq_self]) 2);
    1.33  by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2);
    1.34  (* case n le succ(x) *)
    1.35 -by (asm_full_simp_tac
    1.36 -     (simpset() addsimps [not_lt_iff_le, nat_into_Ord]) 1);
    1.37 +by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1);
    1.38  by (etac leE 1);
    1.39  (*equality case*)
    1.40  by (asm_full_simp_tac (simpset() addsimps [diff_self_eq_0]) 2);
    1.41 @@ -367,8 +365,7 @@
    1.42  by (asm_simp_tac (simpset() addsimps [mod_less]) 2);
    1.43  (*case n le x*)
    1.44  by (asm_full_simp_tac
    1.45 -     (simpset() addsimps [not_lt_iff_le, nat_into_Ord,
    1.46 -                         mod_geq, div_termination RS ltD]) 1);
    1.47 +     (simpset() addsimps [not_lt_iff_le, mod_geq, div_termination RS ltD]) 1);
    1.48  qed "mod_less_divisor";
    1.49  
    1.50  
    1.51 @@ -411,7 +408,7 @@
    1.52  by (ftac lt_nat_in_nat 1);
    1.53  by (assume_tac 1);
    1.54  by (etac succ_lt_induct 1);
    1.55 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_into_Ord, leI])));
    1.56 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI])));
    1.57  qed "add_lt_mono1";
    1.58  
    1.59  (*strict, in both arguments*)
    1.60 @@ -496,7 +493,7 @@
    1.61  by (asm_simp_tac (simpset() addsimps [div_less, zero_lt_mult_iff, 
    1.62                                       mult_lt_mono2]) 2);
    1.63  by (asm_full_simp_tac
    1.64 -     (simpset() addsimps [not_lt_iff_le, nat_into_Ord,
    1.65 +     (simpset() addsimps [not_lt_iff_le, 
    1.66                           zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq,
    1.67                           diff_mult_distrib2 RS sym,
    1.68                           div_termination RS ltD]) 1);
    1.69 @@ -509,7 +506,7 @@
    1.70  by (asm_simp_tac (simpset() addsimps [mod_less, zero_lt_mult_iff, 
    1.71                                       mult_lt_mono2]) 2);
    1.72  by (asm_full_simp_tac
    1.73 -     (simpset() addsimps [not_lt_iff_le, nat_into_Ord,
    1.74 +     (simpset() addsimps [not_lt_iff_le, 
    1.75                           zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq,
    1.76                           diff_mult_distrib2 RS sym,
    1.77                           div_termination RS ltD]) 1);
    1.78 @@ -530,7 +527,7 @@
    1.79  by (induct_tac "m" 1);
    1.80  by (Asm_simp_tac 1);
    1.81  by Safe_tac;
    1.82 -by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt,nat_into_Ord]) 1);
    1.83 +by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt]) 1);
    1.84  qed "add_le_elim1";
    1.85  
    1.86  Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
     2.1 --- a/src/ZF/CardinalArith.ML	Sat Feb 05 17:31:53 2000 +0100
     2.2 +++ b/src/ZF/CardinalArith.ML	Mon Feb 07 15:14:02 2000 +0100
     2.3 @@ -121,7 +121,7 @@
     2.4  Goal "[| m: nat;  n: nat |] ==> m |+| n = m#+n";
     2.5  by (induct_tac "m" 1);
     2.6  by (asm_simp_tac (simpset() addsimps [nat_into_Card RS cadd_0]) 1);
     2.7 -by (asm_simp_tac (simpset() addsimps [nat_into_Ord, cadd_succ_lemma,
     2.8 +by (asm_simp_tac (simpset() addsimps [cadd_succ_lemma,
     2.9  				      nat_into_Card RS Card_cardinal_eq]) 1);
    2.10  qed "nat_cadd_eq_add";
    2.11  
    2.12 @@ -285,8 +285,7 @@
    2.13  Goal "[| m: nat;  n: nat |] ==> m |*| n = m#*n";
    2.14  by (induct_tac "m" 1);
    2.15  by (Asm_simp_tac 1);
    2.16 -by (asm_simp_tac (simpset() addsimps [nat_into_Ord, cmult_succ_lemma,
    2.17 -				      nat_cadd_eq_add]) 1);
    2.18 +by (asm_simp_tac (simpset() addsimps [cmult_succ_lemma, nat_cadd_eq_add]) 1);
    2.19  qed "nat_cmult_eq_mult";
    2.20  
    2.21  Goal "Card(n) ==> 2 |*| n = n |+| n";
     3.1 --- a/src/ZF/Epsilon.ML	Sat Feb 05 17:31:53 2000 +0100
     3.2 +++ b/src/ZF/Epsilon.ML	Mon Feb 07 15:14:02 2000 +0100
     3.3 @@ -107,9 +107,8 @@
     3.4  by (REPEAT (assume_tac 1));
     3.5  qed "mem_eclose_sing_trans";
     3.6  
     3.7 -Goalw [Transset_def]
     3.8 -    "[| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j";
     3.9 -by (blast_tac (claset() addSIs [MemrelI] addSEs [MemrelE]) 1);
    3.10 +Goalw [Transset_def] "[| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j";
    3.11 +by (Blast_tac 1);
    3.12  qed "under_Memrel";
    3.13  
    3.14  (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
    3.15 @@ -318,7 +317,7 @@
    3.16  
    3.17  Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
    3.18  by (rtac (transrec2_def RS def_transrec RS trans) 1);
    3.19 -by (simp_tac (simpset() addsimps [succ_not_0, THE_eq, if_P]) 1);
    3.20 +by (simp_tac (simpset() addsimps [THE_eq, if_P]) 1);
    3.21  by (Blast_tac 1);
    3.22  qed "transrec2_succ";
    3.23  
     4.1 --- a/src/ZF/Finite.ML	Sat Feb 05 17:31:53 2000 +0100
     4.2 +++ b/src/ZF/Finite.ML	Mon Feb 07 15:14:02 2000 +0100
     4.3 @@ -103,7 +103,7 @@
     4.4  (*Functions from a finite ordinal*)
     4.5  Goal "n: nat ==> n->A <= Fin(nat*A)";
     4.6  by (induct_tac "n" 1);
     4.7 -by (simp_tac (simpset() addsimps [Pi_empty1, subset_iff, cons_iff]) 1);
     4.8 +by (simp_tac (simpset() addsimps [subset_iff]) 1);
     4.9  by (asm_simp_tac 
    4.10      (simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
    4.11  by (fast_tac (claset() addSIs [Fin.consI]) 1);
    4.12 @@ -125,14 +125,14 @@
    4.13  
    4.14  Goal "h: A -||>B ==> h: domain(h) -> B";
    4.15  by (etac FiniteFun.induct 1);
    4.16 -by (simp_tac (simpset() addsimps [empty_fun, domain_0]) 1);
    4.17 -by (asm_simp_tac (simpset() addsimps [fun_extend3, domain_cons]) 1);
    4.18 +by (Simp_tac 1);
    4.19 +by (asm_simp_tac (simpset() addsimps [fun_extend3]) 1);
    4.20  qed "FiniteFun_is_fun";
    4.21  
    4.22  Goal "h: A -||>B ==> domain(h) : Fin(A)";
    4.23  by (etac FiniteFun.induct 1);
    4.24 -by (simp_tac (simpset() addsimps [domain_0]) 1);
    4.25 -by (asm_simp_tac (simpset() addsimps [domain_cons]) 1);
    4.26 +by (Simp_tac 1);
    4.27 +by (Asm_simp_tac 1);
    4.28  qed "FiniteFun_domain_Fin";
    4.29  
    4.30  bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type);
     5.1 --- a/src/ZF/Integ/Int.ML	Sat Feb 05 17:31:53 2000 +0100
     5.2 +++ b/src/ZF/Integ/Int.ML	Mon Feb 07 15:14:02 2000 +0100
     5.3 @@ -193,7 +193,7 @@
     5.4  by (rtac bexI 1);
     5.5  by (rtac (add_diff_inverse2 RS sym) 1);
     5.6  by Auto_tac;
     5.7 -by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1);
     5.8 +by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1);
     5.9  qed "not_zneg_int_of";
    5.10  
    5.11  Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
     6.1 --- a/src/ZF/Order.ML	Sat Feb 05 17:31:53 2000 +0100
     6.2 +++ b/src/ZF/Order.ML	Mon Feb 07 15:14:02 2000 +0100
     6.3 @@ -9,8 +9,6 @@
     6.4          by Ken Kunen.  Chapter 1, section 6.
     6.5  *)
     6.6  
     6.7 -open Order;
     6.8 -
     6.9  (** Basic properties of the definitions **)
    6.10  
    6.11  (*needed?*)
    6.12 @@ -567,8 +565,7 @@
    6.13  \       range(ord_iso_map(A,r,B,s)) = B |       \
    6.14  \       (EX y:B. range(ord_iso_map(A,r,B,s))= pred(B,y,s))";
    6.15  by (resolve_tac [converse_ord_iso_map RS subst] 1);
    6.16 -by (asm_simp_tac
    6.17 -    (simpset() addsimps [range_converse, domain_ord_iso_map_cases]) 1);
    6.18 +by (asm_simp_tac (simpset() addsimps [domain_ord_iso_map_cases]) 1);
    6.19  qed "range_ord_iso_map_cases";
    6.20  
    6.21  (*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
     7.1 --- a/src/ZF/OrderArith.ML	Sat Feb 05 17:31:53 2000 +0100
     7.2 +++ b/src/ZF/OrderArith.ML	Mon Feb 07 15:14:02 2000 +0100
     7.3 @@ -6,9 +6,6 @@
     7.4  Towards ordinal arithmetic 
     7.5  *)
     7.6  
     7.7 -open OrderArith;
     7.8 -
     7.9 -
    7.10  (**** Addition of relations -- disjoint sum ****)
    7.11  
    7.12  (** Rewrite rules.  Can be used to obtain introduction rules **)
    7.13 @@ -67,8 +64,7 @@
    7.14  
    7.15  Goalw [linear_def]
    7.16      "[| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))";
    7.17 -by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac sumE));
    7.18 -by (ALLGOALS Asm_simp_tac);
    7.19 +by (Force_tac 1);
    7.20  qed "linear_radd";
    7.21  
    7.22  
    7.23 @@ -110,7 +106,7 @@
    7.24  by (res_inst_tac 
    7.25          [("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(g)`y))")] 
    7.26      lam_bijective 1);
    7.27 -by (safe_tac (claset() addSEs [sumE]));
    7.28 +by Safe_tac;
    7.29  by (ALLGOALS (asm_simp_tac bij_inverse_ss));
    7.30  qed "sum_bij";
    7.31  
    7.32 @@ -134,11 +130,7 @@
    7.33  \           (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)";
    7.34  by (res_inst_tac [("d", "%z. if z:A then Inl(z) else Inr(z)")] 
    7.35      lam_bijective 1);
    7.36 -by (blast_tac (claset() addSIs [if_type]) 2);
    7.37 -by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1));
    7.38 -by Safe_tac;
    7.39 -by (ALLGOALS Asm_simp_tac);
    7.40 -by (blast_tac (claset() addEs [equalityE]) 1);
    7.41 +by Auto_tac;
    7.42  qed "sum_disjoint_bij";
    7.43  
    7.44  (** Associativity **)
    7.45 @@ -147,15 +139,14 @@
    7.46  \ : bij((A+B)+C, A+(B+C))";
    7.47  by (res_inst_tac [("d", "case(%x. Inl(Inl(x)), case(%x. Inl(Inr(x)), Inr))")] 
    7.48      lam_bijective 1);
    7.49 -by (ALLGOALS (asm_simp_tac (simpset() setloop etac sumE)));
    7.50 +by Auto_tac;
    7.51  qed "sum_assoc_bij";
    7.52  
    7.53  Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
    7.54  \ : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),    \
    7.55  \           A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))";
    7.56  by (resolve_tac [sum_assoc_bij RS ord_isoI] 1);
    7.57 -by (REPEAT_FIRST (etac sumE));
    7.58 -by (ALLGOALS Asm_simp_tac);
    7.59 +by Auto_tac;
    7.60  qed "sum_assoc_ord_iso";
    7.61  
    7.62  
    7.63 @@ -255,8 +246,7 @@
    7.64  
    7.65  Goal "(lam z:A. <x,z>) : bij(A, {x}*A)";
    7.66  by (res_inst_tac [("d", "snd")] lam_bijective 1);
    7.67 -by Safe_tac;
    7.68 -by (ALLGOALS Asm_simp_tac);
    7.69 +by Auto_tac;
    7.70  qed "singleton_prod_bij";
    7.71  
    7.72  (*Used??*)
    7.73 @@ -277,7 +267,7 @@
    7.74  by (rtac singleton_prod_bij 1);
    7.75  by (rtac sum_disjoint_bij 1);
    7.76  by (Blast_tac 1);
    7.77 -by (asm_simp_tac (simpset() addcongs [case_cong] addsimps [id_conv]) 1);
    7.78 +by (asm_simp_tac (simpset() addcongs [case_cong]) 1);
    7.79  by (resolve_tac [comp_lam RS trans RS sym] 1);
    7.80  by (fast_tac (claset() addSEs [case_type]) 1);
    7.81  by (asm_simp_tac (simpset() addsimps [case_case]) 1);
    7.82 @@ -303,40 +293,35 @@
    7.83  \ : bij((A+B)*C, (A*C)+(B*C))";
    7.84  by (res_inst_tac
    7.85      [("d", "case(%<x,y>.<Inl(x),y>, %<x,y>.<Inr(x),y>)")] lam_bijective 1);
    7.86 -by (safe_tac (claset() addSEs [sumE]));
    7.87 -by (ALLGOALS Asm_simp_tac);
    7.88 +by Auto_tac;
    7.89  qed "sum_prod_distrib_bij";
    7.90  
    7.91  Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
    7.92  \ : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), \
    7.93  \           (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))";
    7.94  by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1);
    7.95 -by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE]));
    7.96 -by (ALLGOALS Asm_simp_tac);
    7.97 +by Auto_tac;
    7.98  qed "sum_prod_distrib_ord_iso";
    7.99  
   7.100  (** Associativity **)
   7.101  
   7.102  Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))";
   7.103  by (res_inst_tac [("d", "%<x, <y,z>>. <<x,y>, z>")] lam_bijective 1);
   7.104 -by (ALLGOALS (asm_simp_tac (simpset() setloop etac SigmaE)));
   7.105 +by Auto_tac;
   7.106  qed "prod_assoc_bij";
   7.107  
   7.108  Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)                   \
   7.109  \ : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),  \
   7.110  \           A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))";
   7.111  by (resolve_tac [prod_assoc_bij RS ord_isoI] 1);
   7.112 -by (REPEAT_FIRST (eresolve_tac [SigmaE, ssubst]));
   7.113 -by (Asm_simp_tac 1);
   7.114 -by (Blast_tac 1);
   7.115 +by Auto_tac;
   7.116  qed "prod_assoc_ord_iso";
   7.117  
   7.118  (**** Inverse image of a relation ****)
   7.119  
   7.120  (** Rewrite rule **)
   7.121  
   7.122 -Goalw [rvimage_def] 
   7.123 -    "<a,b> : rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A";
   7.124 +Goalw [rvimage_def] "<a,b> : rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A";
   7.125  by (Blast_tac 1);
   7.126  qed "rvimage_iff";
   7.127  
   7.128 @@ -348,8 +333,7 @@
   7.129  
   7.130  bind_thm ("field_rvimage", (rvimage_type RS field_rel_subset));
   7.131  
   7.132 -Goalw [rvimage_def] 
   7.133 -    "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))";
   7.134 +Goalw [rvimage_def] "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))";
   7.135  by (Blast_tac 1);
   7.136  qed "rvimage_converse";
   7.137  
   7.138 @@ -398,7 +382,7 @@
   7.139  by (eres_inst_tac [("a","f`y")] wf_on_induct 1);
   7.140  by (blast_tac (claset() addSIs [apply_funtype]) 1);
   7.141  by (blast_tac (claset() addSIs [apply_funtype] 
   7.142 -                       addSDs [rvimage_iff RS iffD1]) 1);
   7.143 +                        addSDs [rvimage_iff RS iffD1]) 1);
   7.144  qed "wf_on_rvimage";
   7.145  
   7.146  (*Note that we need only wf[A](...) and linear(A,...) to get the result!*)
     8.1 --- a/src/ZF/Resid/Substitution.ML	Sat Feb 05 17:31:53 2000 +0100
     8.2 +++ b/src/ZF/Resid/Substitution.ML	Mon Feb 07 15:14:02 2000 +0100
     8.3 @@ -34,7 +34,7 @@
     8.4  qed "gt_pred";
     8.5  
     8.6  
     8.7 -Addsimps [nat_into_Ord, not_lt_iff_le, if_P, if_not_P];
     8.8 +Addsimps [not_lt_iff_le, if_P, if_not_P];
     8.9  
    8.10  
    8.11  (* ------------------------------------------------------------------------- *)
     9.1 --- a/src/ZF/Sum.ML	Sat Feb 05 17:31:53 2000 +0100
     9.2 +++ b/src/ZF/Sum.ML	Mon Feb 07 15:14:02 2000 +0100
     9.3 @@ -131,11 +131,11 @@
     9.4  (*** Eliminator -- case ***)
     9.5  
     9.6  Goalw sum_defs "case(c, d, Inl(a)) = c(a)";
     9.7 -by (simp_tac (simpset() addsimps [cond_0]) 1);
     9.8 +by (Simp_tac 1);
     9.9  qed "case_Inl";
    9.10  
    9.11  Goalw sum_defs "case(c, d, Inr(b)) = d(b)";
    9.12 -by (simp_tac (simpset() addsimps [cond_1]) 1);
    9.13 +by (Simp_tac 1);
    9.14  qed "case_Inr";
    9.15  
    9.16  Addsimps [case_Inl, case_Inr];
    10.1 --- a/src/ZF/ex/Limit.ML	Sat Feb 05 17:31:53 2000 +0100
    10.2 +++ b/src/ZF/ex/Limit.ML	Mon Feb 07 15:14:02 2000 +0100
    10.3 @@ -1784,7 +1784,6 @@
    10.4  (* Must control rewriting by instantiating a variable. *)
    10.5  by (asm_full_simp_tac(simpset() addsimps
    10.6       [read_instantiate [("i1","n")] (nat_into_Ord RS not_le_iff_lt RS iff_sym),
    10.7 -      nat_into_Ord,
    10.8        add_le_self]) 1);
    10.9  qed "eps_e_gr_add";
   10.10  
    11.1 --- a/src/ZF/ex/Primrec.ML	Sat Feb 05 17:31:53 2000 +0100
    11.2 +++ b/src/ZF/ex/Primrec.ML	Mon Feb 07 15:14:02 2000 +0100
    11.3 @@ -52,7 +52,7 @@
    11.4  by (asm_simp_tac (simpset() addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
    11.5  qed "ack_succ_succ";
    11.6  
    11.7 -Addsimps [ack_0, ack_succ_0, ack_succ_succ, ack_type, nat_into_Ord];
    11.8 +Addsimps [ack_0, ack_succ_0, ack_succ_succ, ack_type];
    11.9  Delsimps [ACK_0, ACK_succ];
   11.10  
   11.11  
   11.12 @@ -165,7 +165,7 @@
   11.13  
   11.14  (*** MAIN RESULT ***)
   11.15  
   11.16 -Addsimps [list_add_type, nat_into_Ord];
   11.17 +Addsimps [list_add_type];
   11.18  
   11.19  Goalw [SC_def] "l: list(nat) ==> SC ` l < ack(1, list_add(l))";
   11.20  by (exhaust_tac "l" 1);
    12.1 --- a/src/ZF/func.ML	Sat Feb 05 17:31:53 2000 +0100
    12.2 +++ b/src/ZF/func.ML	Mon Feb 07 15:14:02 2000 +0100
    12.3 @@ -353,7 +353,7 @@
    12.4  
    12.5  (** The Union of 2 disjoint functions is a function **)
    12.6  
    12.7 -val Un_rls = [Un_subset_iff, domain_Un_eq, SUM_Un_distrib1, prod_Un_distrib2, 
    12.8 +val Un_rls = [Un_subset_iff, SUM_Un_distrib1, prod_Un_distrib2, 
    12.9                Un_upper1 RSN (2, subset_trans), 
   12.10                Un_upper2 RSN (2, subset_trans)];
   12.11