# HG changeset patch
# User paulson
# Date 865596520 -7200
# Node ID e7cef2081106eee93b7ffb241053a43fda54890b
# Parent  9aa5864a7eea3da46c85151d09d186f69c59df8c
Removed a few redundant additions of simprules or classical rules

diff -r 9aa5864a7eea -r e7cef2081106 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Fri Jun 06 13:26:41 1997 +0200
+++ b/src/HOL/Divides.ML	Fri Jun 06 13:28:40 1997 +0200
@@ -178,7 +178,7 @@
 goal thy "(m+m) mod 2 = 0";
 by (induct_tac "m" 1);
 by (simp_tac (!simpset addsimps [mod_less]) 1);
-by (asm_simp_tac (!simpset addsimps [mod2_Suc_Suc, add_Suc_right]) 1);
+by (Asm_simp_tac 1);
 qed "mod2_add_self";
 Addsimps [mod2_add_self];
 
diff -r 9aa5864a7eea -r e7cef2081106 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Fri Jun 06 13:26:41 1997 +0200
+++ b/src/HOL/Finite.ML	Fri Jun 06 13:28:40 1997 +0200
@@ -83,7 +83,7 @@
 goal Finite.thy "finite(insert a A) = finite A";
 by (stac insert_is_Un 1);
 by (simp_tac (HOL_ss addsimps [finite_Un]) 1);
-by (blast_tac (!claset addSIs Finites.intrs) 1);
+by (Blast_tac 1);
 qed "finite_insert";
 Addsimps[finite_insert];
 
diff -r 9aa5864a7eea -r e7cef2081106 src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Fri Jun 06 13:26:41 1997 +0200
+++ b/src/HOL/Induct/LList.ML	Fri Jun 06 13:28:40 1997 +0200
@@ -27,7 +27,7 @@
 
 goal LList.thy "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
 let val rew = rewrite_rule [NIL_def, CONS_def] in  
-by (fast_tac (!claset addSIs (equalityI :: map rew llist.intrs)
+by (fast_tac (!claset addSIs (map rew llist.intrs)
                       addEs [rew llist.elim]) 1)
 end;
 qed "llist_unfold";
@@ -148,7 +148,7 @@
 (*This theorem is actually used, unlike the many similar ones in ZF*)
 goal LList.thy "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))";
 let val rew = rewrite_rule [NIL_def, CONS_def] in  
-by (fast_tac (!claset addSIs (equalityI :: map rew LListD.intrs)
+by (fast_tac (!claset addSIs (map rew LListD.intrs)
                       addEs [rew LListD.elim]) 1)
 end;
 qed "LListD_unfold";
@@ -157,7 +157,7 @@
 by (res_inst_tac [("n", "k")] less_induct 1);
 by (safe_tac ((claset_of "Fun") delrules [equalityI]));
 by (etac LListD.elim 1);
-by (safe_tac (((claset_of "Prod") delrules [equalityI]) addSEs [diagE]));
+by (safe_tac (claset_of "Prod" delrules [equalityI] addSEs [diagE]));
 by (res_inst_tac [("n", "n")] natE 1);
 by (asm_simp_tac (!simpset addsimps [ntrunc_0]) 1);
 by (rename_tac "n'" 1);
@@ -392,7 +392,7 @@
 (** Injectiveness of CONS and LCons **)
 
 goalw LList.thy [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')";
-by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
+by (fast_tac (!claset addSEs [Scons_inject]) 1);
 qed "CONS_CONS_eq2";
 
 bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
diff -r 9aa5864a7eea -r e7cef2081106 src/HOL/Induct/Term.ML
--- a/src/HOL/Induct/Term.ML	Fri Jun 06 13:26:41 1997 +0200
+++ b/src/HOL/Induct/Term.ML	Fri Jun 06 13:28:40 1997 +0200
@@ -12,7 +12,7 @@
 (*** Monotonicity and unfolding of the function ***)
 
 goal Term.thy "term(A) = A <*> list(term(A))";
-by (fast_tac (!claset addSIs (equalityI :: term.intrs)
+by (fast_tac (!claset addSIs term.intrs
                       addEs [term.elim]) 1);
 qed "term_unfold";
 
diff -r 9aa5864a7eea -r e7cef2081106 src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Fri Jun 06 13:26:41 1997 +0200
+++ b/src/HOL/Integ/Equiv.ML	Fri Jun 06 13:28:40 1997 +0200
@@ -39,8 +39,8 @@
 by (etac equalityE 1);
 by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
 by (Step_tac 1);
-by (fast_tac (!claset addSIs [converseI] addIs [compI]) 3);
-by (ALLGOALS (fast_tac (!claset addIs [compI] addSEs [compE])));
+by (fast_tac (!claset addIs [compI]) 3);
+by (ALLGOALS (fast_tac (!claset addIs [compI])));
 qed "comp_equivI";
 
 (** Equivalence classes **)
diff -r 9aa5864a7eea -r e7cef2081106 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Fri Jun 06 13:26:41 1997 +0200
+++ b/src/HOL/Univ.ML	Fri Jun 06 13:28:40 1997 +0200
@@ -257,7 +257,7 @@
 
 goalw Univ.thy [Scons_def,ntrunc_def]
     "ntrunc (Suc k) (M$N) = ntrunc k M $ ntrunc k N";
-by (safe_tac (!claset addSIs [equalityI, imageI]));
+by (safe_tac (!claset addSIs [imageI]));
 by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
 by (REPEAT (rtac Suc_less_SucD 1 THEN 
             rtac (ndepth_Push_Node RS subst) 1 THEN