# HG changeset patch
# User wenzelm
# Date 1329235893 -3600
# Node ID 73823dbbecc40d634858df124a19a142b8825cf7
# Parent  19ef91d7fbd4b0561b0576a3af21574bfeb03f1b
eliminated obsolete aliases;

diff -r 19ef91d7fbd4 -r 73823dbbecc4 src/HOL/IMPP/Natural.thy
--- a/src/HOL/IMPP/Natural.thy	Tue Feb 14 16:59:12 2012 +0100
+++ b/src/HOL/IMPP/Natural.thy	Tue Feb 14 17:11:33 2012 +0100
@@ -140,7 +140,7 @@
 lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
 apply (erule evalc.induct)
 apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
-apply (tactic {* TRYALL (EVERY' [datac @{thm evaln_max2} 1, REPEAT o eresolve_tac [exE, conjE]]) *})
+apply (tactic {* TRYALL (EVERY' [dtac @{thm evaln_max2}, assume_tac, REPEAT o eresolve_tac [exE, conjE]]) *})
 apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
 done
 
diff -r 19ef91d7fbd4 -r 73823dbbecc4 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Feb 14 16:59:12 2012 +0100
+++ b/src/HOL/Set.thy	Tue Feb 14 17:11:33 2012 +0100
@@ -379,7 +379,7 @@
 *}
 
 declaration {* fn _ =>
-  Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
+  Classical.map_cs (fn cs => cs addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac))
 *}
 
 ML {*
diff -r 19ef91d7fbd4 -r 73823dbbecc4 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Feb 14 16:59:12 2012 +0100
+++ b/src/Provers/classical.ML	Tue Feb 14 17:11:33 2012 +0100
@@ -670,8 +670,8 @@
 fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
 fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
 
-fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
-fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
+fun cs addD2 (name, thm) = cs addafter (name, dtac thm THEN' assume_tac);
+fun cs addE2 (name, thm) = cs addafter (name, etac thm THEN' assume_tac);
 fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
 fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
 
diff -r 19ef91d7fbd4 -r 73823dbbecc4 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue Feb 14 16:59:12 2012 +0100
+++ b/src/Pure/tactic.ML	Tue Feb 14 17:11:33 2012 +0100
@@ -22,9 +22,6 @@
   val dtac: thm -> int -> tactic
   val etac: thm -> int -> tactic
   val ftac: thm -> int -> tactic
-  val datac: thm -> int -> int -> tactic
-  val eatac: thm -> int -> int -> tactic
-  val fatac: thm -> int -> int -> tactic
   val ares_tac: thm list -> int -> tactic
   val solve_tac: thm list -> int -> tactic
   val bimatch_tac: (bool * thm) list -> int -> tactic
@@ -140,9 +137,6 @@
 fun dtac rl = dresolve_tac [rl];
 fun etac rl = eresolve_tac [rl];
 fun ftac rl =  forward_tac [rl];
-fun datac thm j = EVERY' (dtac thm::replicate j atac);
-fun eatac thm j = EVERY' (etac thm::replicate j atac);
-fun fatac thm j = EVERY' (ftac thm::replicate j atac);
 
 (*Use an assumption or some rules ... A popular combination!*)
 fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;