# HG changeset patch
# User wenzelm
# Date 1437942371 -7200
# Node ID bbcd4ab6d26ee2bf845012852d6b9feae0f85267
# Parent  722cb21ab680b5225768cec21639a64e5733a048
eliminated atac, rtac, etac, dtac, ftac;

diff -r 722cb21ab680 -r bbcd4ab6d26e NEWS
--- a/NEWS	Sun Jul 26 22:19:14 2015 +0200
+++ b/NEWS	Sun Jul 26 22:26:11 2015 +0200
@@ -244,7 +244,11 @@
 command. Minor INCOMPATIBILITY, use 'function' instead.
 
 
-** ML **
+*** ML ***
+
+* Old tactic shorthands atac, rtac, etac, dtac, ftac have been
+discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
+instead (with proper context).
 
 * Thm.instantiate (and derivatives) no longer require the LHS of the
 instantiation to be certified: plain variables are given directly.
diff -r 722cb21ab680 -r bbcd4ab6d26e src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Sun Jul 26 22:19:14 2015 +0200
+++ b/src/Pure/tactic.ML	Sun Jul 26 22:26:11 2015 +0200
@@ -21,10 +21,6 @@
   val forward_tac: Proof.context -> thm list -> int -> tactic
   val dresolve0_tac: thm list -> int -> tactic
   val dresolve_tac: Proof.context -> thm list -> int -> tactic
-  val atac: int -> tactic
-  val rtac: thm -> int -> tactic
-  val dtac: thm -> int -> tactic
-  val etac: thm -> int -> tactic
   val ares_tac: Proof.context -> thm list -> int -> tactic
   val solve_tac: Proof.context -> thm list -> int -> tactic
   val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic
@@ -99,7 +95,6 @@
 
 (*Solve subgoal i by assumption*)
 fun assume_tac ctxt i = PRIMSEQ (Thm.assumption (SOME ctxt) i);
-fun atac i = PRIMSEQ (Thm.assumption NONE i);
 
 (*Solve subgoal i by assumption, using no unification*)
 fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i);
@@ -135,11 +130,6 @@
 fun dresolve0_tac rls = eresolve0_tac (map make_elim rls);
 fun dresolve_tac ctxt rls = eresolve_tac ctxt (map make_elim rls);
 
-(*Shorthand versions: for resolution with a single theorem*)
-fun rtac rl =  resolve0_tac [rl];
-fun dtac rl = dresolve0_tac [rl];
-fun etac rl = eresolve0_tac [rl];
-
 (*Use an assumption or some rules*)
 fun ares_tac ctxt rules = assume_tac ctxt ORELSE' resolve_tac ctxt rules;