Removed a few redundant additions of simprules or classical rules
authorpaulson
Fri Jun 06 13:28:40 1997 +0200 (1997-06-06)
changeset 3427e7cef2081106
parent 3426 9aa5864a7eea
child 3428 34655a5d2f56
Removed a few redundant additions of simprules or classical rules
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/Induct/LList.ML
src/HOL/Induct/Term.ML
src/HOL/Integ/Equiv.ML
src/HOL/Univ.ML
     1.1 --- a/src/HOL/Divides.ML	Fri Jun 06 13:26:41 1997 +0200
     1.2 +++ b/src/HOL/Divides.ML	Fri Jun 06 13:28:40 1997 +0200
     1.3 @@ -178,7 +178,7 @@
     1.4  goal thy "(m+m) mod 2 = 0";
     1.5  by (induct_tac "m" 1);
     1.6  by (simp_tac (!simpset addsimps [mod_less]) 1);
     1.7 -by (asm_simp_tac (!simpset addsimps [mod2_Suc_Suc, add_Suc_right]) 1);
     1.8 +by (Asm_simp_tac 1);
     1.9  qed "mod2_add_self";
    1.10  Addsimps [mod2_add_self];
    1.11  
     2.1 --- a/src/HOL/Finite.ML	Fri Jun 06 13:26:41 1997 +0200
     2.2 +++ b/src/HOL/Finite.ML	Fri Jun 06 13:28:40 1997 +0200
     2.3 @@ -83,7 +83,7 @@
     2.4  goal Finite.thy "finite(insert a A) = finite A";
     2.5  by (stac insert_is_Un 1);
     2.6  by (simp_tac (HOL_ss addsimps [finite_Un]) 1);
     2.7 -by (blast_tac (!claset addSIs Finites.intrs) 1);
     2.8 +by (Blast_tac 1);
     2.9  qed "finite_insert";
    2.10  Addsimps[finite_insert];
    2.11  
     3.1 --- a/src/HOL/Induct/LList.ML	Fri Jun 06 13:26:41 1997 +0200
     3.2 +++ b/src/HOL/Induct/LList.ML	Fri Jun 06 13:28:40 1997 +0200
     3.3 @@ -27,7 +27,7 @@
     3.4  
     3.5  goal LList.thy "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
     3.6  let val rew = rewrite_rule [NIL_def, CONS_def] in  
     3.7 -by (fast_tac (!claset addSIs (equalityI :: map rew llist.intrs)
     3.8 +by (fast_tac (!claset addSIs (map rew llist.intrs)
     3.9                        addEs [rew llist.elim]) 1)
    3.10  end;
    3.11  qed "llist_unfold";
    3.12 @@ -148,7 +148,7 @@
    3.13  (*This theorem is actually used, unlike the many similar ones in ZF*)
    3.14  goal LList.thy "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))";
    3.15  let val rew = rewrite_rule [NIL_def, CONS_def] in  
    3.16 -by (fast_tac (!claset addSIs (equalityI :: map rew LListD.intrs)
    3.17 +by (fast_tac (!claset addSIs (map rew LListD.intrs)
    3.18                        addEs [rew LListD.elim]) 1)
    3.19  end;
    3.20  qed "LListD_unfold";
    3.21 @@ -157,7 +157,7 @@
    3.22  by (res_inst_tac [("n", "k")] less_induct 1);
    3.23  by (safe_tac ((claset_of "Fun") delrules [equalityI]));
    3.24  by (etac LListD.elim 1);
    3.25 -by (safe_tac (((claset_of "Prod") delrules [equalityI]) addSEs [diagE]));
    3.26 +by (safe_tac (claset_of "Prod" delrules [equalityI] addSEs [diagE]));
    3.27  by (res_inst_tac [("n", "n")] natE 1);
    3.28  by (asm_simp_tac (!simpset addsimps [ntrunc_0]) 1);
    3.29  by (rename_tac "n'" 1);
    3.30 @@ -392,7 +392,7 @@
    3.31  (** Injectiveness of CONS and LCons **)
    3.32  
    3.33  goalw LList.thy [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')";
    3.34 -by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
    3.35 +by (fast_tac (!claset addSEs [Scons_inject]) 1);
    3.36  qed "CONS_CONS_eq2";
    3.37  
    3.38  bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
     4.1 --- a/src/HOL/Induct/Term.ML	Fri Jun 06 13:26:41 1997 +0200
     4.2 +++ b/src/HOL/Induct/Term.ML	Fri Jun 06 13:28:40 1997 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4  (*** Monotonicity and unfolding of the function ***)
     4.5  
     4.6  goal Term.thy "term(A) = A <*> list(term(A))";
     4.7 -by (fast_tac (!claset addSIs (equalityI :: term.intrs)
     4.8 +by (fast_tac (!claset addSIs term.intrs
     4.9                        addEs [term.elim]) 1);
    4.10  qed "term_unfold";
    4.11  
     5.1 --- a/src/HOL/Integ/Equiv.ML	Fri Jun 06 13:26:41 1997 +0200
     5.2 +++ b/src/HOL/Integ/Equiv.ML	Fri Jun 06 13:28:40 1997 +0200
     5.3 @@ -39,8 +39,8 @@
     5.4  by (etac equalityE 1);
     5.5  by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
     5.6  by (Step_tac 1);
     5.7 -by (fast_tac (!claset addSIs [converseI] addIs [compI]) 3);
     5.8 -by (ALLGOALS (fast_tac (!claset addIs [compI] addSEs [compE])));
     5.9 +by (fast_tac (!claset addIs [compI]) 3);
    5.10 +by (ALLGOALS (fast_tac (!claset addIs [compI])));
    5.11  qed "comp_equivI";
    5.12  
    5.13  (** Equivalence classes **)
     6.1 --- a/src/HOL/Univ.ML	Fri Jun 06 13:26:41 1997 +0200
     6.2 +++ b/src/HOL/Univ.ML	Fri Jun 06 13:28:40 1997 +0200
     6.3 @@ -257,7 +257,7 @@
     6.4  
     6.5  goalw Univ.thy [Scons_def,ntrunc_def]
     6.6      "ntrunc (Suc k) (M$N) = ntrunc k M $ ntrunc k N";
     6.7 -by (safe_tac (!claset addSIs [equalityI, imageI]));
     6.8 +by (safe_tac (!claset addSIs [imageI]));
     6.9  by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
    6.10  by (REPEAT (rtac Suc_less_SucD 1 THEN 
    6.11              rtac (ndepth_Push_Node RS subst) 1 THEN