--- 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.
--- 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;