# 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