eliminated atac, rtac, etac, dtac, ftac;
authorwenzelm
Sun Jul 26 22:26:11 2015 +0200 (2015-07-26)
changeset 60793bbcd4ab6d26e
parent 60792 722cb21ab680
child 60794 f21f70d24844
eliminated atac, rtac, etac, dtac, ftac;
NEWS
src/Pure/tactic.ML
     1.1 --- a/NEWS	Sun Jul 26 22:19:14 2015 +0200
     1.2 +++ b/NEWS	Sun Jul 26 22:26:11 2015 +0200
     1.3 @@ -244,7 +244,11 @@
     1.4  command. Minor INCOMPATIBILITY, use 'function' instead.
     1.5  
     1.6  
     1.7 -** ML **
     1.8 +*** ML ***
     1.9 +
    1.10 +* Old tactic shorthands atac, rtac, etac, dtac, ftac have been
    1.11 +discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
    1.12 +instead (with proper context).
    1.13  
    1.14  * Thm.instantiate (and derivatives) no longer require the LHS of the
    1.15  instantiation to be certified: plain variables are given directly.
     2.1 --- a/src/Pure/tactic.ML	Sun Jul 26 22:19:14 2015 +0200
     2.2 +++ b/src/Pure/tactic.ML	Sun Jul 26 22:26:11 2015 +0200
     2.3 @@ -21,10 +21,6 @@
     2.4    val forward_tac: Proof.context -> thm list -> int -> tactic
     2.5    val dresolve0_tac: thm list -> int -> tactic
     2.6    val dresolve_tac: Proof.context -> thm list -> int -> tactic
     2.7 -  val atac: int -> tactic
     2.8 -  val rtac: thm -> int -> tactic
     2.9 -  val dtac: thm -> int -> tactic
    2.10 -  val etac: thm -> int -> tactic
    2.11    val ares_tac: Proof.context -> thm list -> int -> tactic
    2.12    val solve_tac: Proof.context -> thm list -> int -> tactic
    2.13    val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic
    2.14 @@ -99,7 +95,6 @@
    2.15  
    2.16  (*Solve subgoal i by assumption*)
    2.17  fun assume_tac ctxt i = PRIMSEQ (Thm.assumption (SOME ctxt) i);
    2.18 -fun atac i = PRIMSEQ (Thm.assumption NONE i);
    2.19  
    2.20  (*Solve subgoal i by assumption, using no unification*)
    2.21  fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i);
    2.22 @@ -135,11 +130,6 @@
    2.23  fun dresolve0_tac rls = eresolve0_tac (map make_elim rls);
    2.24  fun dresolve_tac ctxt rls = eresolve_tac ctxt (map make_elim rls);
    2.25  
    2.26 -(*Shorthand versions: for resolution with a single theorem*)
    2.27 -fun rtac rl =  resolve0_tac [rl];
    2.28 -fun dtac rl = dresolve0_tac [rl];
    2.29 -fun etac rl = eresolve0_tac [rl];
    2.30 -
    2.31  (*Use an assumption or some rules*)
    2.32  fun ares_tac ctxt rules = assume_tac ctxt ORELSE' resolve_tac ctxt rules;
    2.33