1.1 --- a/doc-src/Ref/tactic.tex	Mon Sep 06 18:17:48 1999 +0200
     1.2 +++ b/doc-src/Ref/tactic.tex	Mon Sep 06 18:18:09 1999 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4    elimination rules.  It resolves with a rule, proves its first premise by
     1.5    assumption, and finally \emph{deletes} that assumption from any new
     1.6    subgoals.  (To rotate a rule's premises,
     1.7 -  see \texttt{rotate_prems} in~\S\ref{MiscellaneousForwardRules}.)
     1.8 +  see \texttt{rotate_prems} in~{\S}\ref{MiscellaneousForwardRules}.)
     1.9  
    1.10  \item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] 
    1.11    \index{forward proof}\index{destruct-resolution}
    1.12 @@ -170,12 +170,16 @@
    1.13  \index{tactics!resolution}\index{tactics!assumption}
    1.14  \index{tactics!meta-rewriting}
    1.15  \begin{ttbox} 
    1.16 -rtac     :      thm -> int -> tactic
    1.17 -etac     :      thm -> int -> tactic
    1.18 -dtac     :      thm -> int -> tactic
    1.19 -atac     :             int -> tactic
    1.20 -ares_tac : thm list -> int -> tactic
    1.21 -rewtac   :      thm ->        tactic
    1.22 +rtac     :      thm ->        int -> tactic
    1.23 +etac     :      thm ->        int -> tactic
    1.24 +dtac     :      thm ->        int -> tactic
    1.25 +ftac     :      thm ->        int -> tactic
    1.26 +atac     :                    int -> tactic
    1.27 +eatac    :      thm -> int -> int -> tactic
    1.28 +datac    :      thm -> int -> int -> tactic
    1.29 +fatac    :      thm -> int -> int -> tactic
    1.30 +ares_tac :      thm list   -> int -> tactic
    1.31 +rewtac   :      thm ->               tactic
    1.32  \end{ttbox}
    1.33  These abbreviate common uses of tactics.
    1.34  \begin{ttdescription}
    1.35 @@ -189,9 +193,25 @@
    1.36  abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
    1.37  destruct-resolution.
    1.38  
    1.39 +\item[\ttindexbold{ftac} {\it thm} {\it i}] 
    1.40 +abbreviates \hbox{\tt forward_tac [{\it thm}] {\it i}}, doing
    1.41 +destruct-resolution without deleting the assumption.
    1.42 +
    1.43  \item[\ttindexbold{atac} {\it i}] 
    1.44  abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
    1.45  
    1.46 +\item[\ttindexbold{eatac} {\it thm} {\it j} {\it i}] 
    1.47 +performs \hbox{\tt etac {\it thm}} and then {\it j} times \texttt{atac}, 
    1.48 +solving additionally {\it j}~premises of the rule {\it thm} by assumption.
    1.49 +
    1.50 +\item[\ttindexbold{datac} {\it thm} {\it j} {\it i}] 
    1.51 +performs \hbox{\tt dtac {\it thm}} and then {\it j} times \texttt{atac}, 
    1.52 +solving additionally {\it j}~premises of the rule {\it thm} by assumption.
    1.53 +
    1.54 +\item[\ttindexbold{fatac} {\it thm} {\it j} {\it i}] 
    1.55 +performs \hbox{\tt ftac {\it thm}} and then {\it j} times \texttt{atac}, 
    1.56 +solving additionally {\it j}~premises of the rule {\it thm} by assumption.
    1.57 +
    1.58  \item[\ttindexbold{ares_tac} {\it thms} {\it i}] 
    1.59  tries proof by assumption and resolution; it abbreviates
    1.60  \begin{ttbox}
    1.61 @@ -224,7 +244,7 @@
    1.62  
    1.63  \item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
    1.64    instantiates the {\it thm} with the instantiations {\it insts}, as
    1.65 -  described in \S\ref{res_inst_tac}.  It adds the resulting theorem as a
    1.66 +  described in {\S}\ref{res_inst_tac}.  It adds the resulting theorem as a
    1.67    new assumption to subgoal~$i$. 
    1.68  
    1.69  \item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] 
    1.70 @@ -419,7 +439,7 @@
    1.71  
    1.72    Flex-flex constraints arise from difficult cases of higher-order
    1.73    unification.  To prevent this, use \ttindex{res_inst_tac} to instantiate
    1.74 -  some variables in a rule~(\S\ref{res_inst_tac}).  Normally flex-flex
    1.75 +  some variables in a rule~({\S}\ref{res_inst_tac}).  Normally flex-flex
    1.76    constraints can be ignored; they often disappear as unknowns get
    1.77    instantiated.
    1.78  \end{ttdescription}
    1.79 @@ -473,7 +493,7 @@
    1.80  
    1.81  \item[\ttindexbold{bimatch_tac}] 
    1.82  is like {\tt biresolve_tac}, but performs matching: unknowns in the
    1.83 -proof state are never updated (see~\S\ref{match_tac}).
    1.84 +proof state are never updated (see~{\S}\ref{match_tac}).
    1.85  
    1.86  \item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})] 
    1.87  returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the

     2.1 --- a/lib/scripts/expandshort.pl	Mon Sep 06 18:17:48 1999 +0200
     2.2 +++ b/lib/scripts/expandshort.pl	Mon Sep 06 18:18:09 1999 +0200
     2.3 @@ -33,6 +33,7 @@
     2.4      s/\bauto *\(\)/by Auto_tac/sg;
     2.5      s/dresolve_tac *\[(\w+)\] */dtac $1 /sg;
     2.6      s/eresolve_tac *\[(\w+)\] */etac $1 /sg;
     2.7 +    s/forward_tac *\[(\w+)\] */ftac $1 /sg;
     2.8      s/resolve_tac *\[(\w+)\] */rtac $1 /sg;
     2.9      s/rewrite_goals_tac *\[(\w+)\]( *)/rewtac $1$2/sg;
    2.10      s/rtac *\((\w+)\s+RS\s+ssubst\)\s+/stac $1 /sg;

     3.1 --- a/src/Pure/tactic.ML	Mon Sep 06 18:17:48 1999 +0200
     3.2 +++ b/src/Pure/tactic.ML	Mon Sep 06 18:18:09 1999 +0200
     3.3 @@ -30,17 +30,20 @@
     3.4    val compose_tac	: (bool * thm * int) -> int -> tactic 
     3.5    val cut_facts_tac	: thm list -> int -> tactic
     3.6    val cut_inst_tac	: (string*string)list -> thm -> int -> tactic   
     3.7 +  val datac             : thm -> int -> int -> tactic
     3.8    val defer_tac 	: int -> tactic
     3.9    val distinct_subgoals_tac	: tactic
    3.10    val dmatch_tac	: thm list -> int -> tactic
    3.11    val dresolve_tac	: thm list -> int -> tactic
    3.12    val dres_inst_tac	: (string*string)list -> thm -> int -> tactic   
    3.13    val dtac		: thm -> int ->tactic
    3.14 +  val eatac             : thm -> int -> int -> tactic
    3.15    val etac		: thm -> int ->tactic
    3.16    val eq_assume_tac	: int -> tactic   
    3.17    val ematch_tac	: thm list -> int -> tactic
    3.18    val eresolve_tac	: thm list -> int -> tactic
    3.19    val eres_inst_tac	: (string*string)list -> thm -> int -> tactic
    3.20 +  val fatac             : thm -> int -> int -> tactic
    3.21    val filter_prems_tac  : (term -> bool) -> int -> tactic  
    3.22    val filter_thms	: (term*term->bool) -> int*term*thm list -> thm list
    3.23    val filt_resolve_tac	: thm list -> int -> int -> tactic
    3.24 @@ -49,6 +52,7 @@
    3.25    val fold_tac		: thm list -> tactic
    3.26    val forward_tac	: thm list -> int -> tactic   
    3.27    val forw_inst_tac	: (string*string)list -> thm -> int -> tactic
    3.28 +  val ftac		: thm -> int ->tactic
    3.29    val insert_tagged_brl : ('a*(bool*thm)) * 
    3.30                            (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
    3.31                            ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
    3.32 @@ -156,10 +160,14 @@
    3.33  fun dresolve_tac rls = eresolve_tac (map make_elim rls);
    3.34  
    3.35  (*Shorthand versions: for resolution with a single theorem*)
    3.36 -fun rtac rl = resolve_tac [rl];
    3.37 +val atac    =   assume_tac;
    3.38 +fun rtac rl =  resolve_tac [rl];
    3.39 +fun dtac rl = dresolve_tac [rl];
    3.40  fun etac rl = eresolve_tac [rl];
    3.41 -fun dtac rl = dresolve_tac [rl];
    3.42 -val atac = assume_tac;
    3.43 +fun ftac rl =  forward_tac [rl];
    3.44 +fun datac thm j = EVERY' (dtac thm::replicate j atac);
    3.45 +fun eatac thm j = EVERY' (etac thm::replicate j atac);
    3.46 +fun fatac thm j = EVERY' (ftac thm::replicate j atac);
    3.47  
    3.48  (*Use an assumption or some rules ... A popular combination!*)
    3.49  fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;