1.1 --- a/doc-src/Ref/tactic.tex	Mon Mar 21 10:51:28 1994 +0100
     1.2 +++ b/doc-src/Ref/tactic.tex	Mon Mar 21 11:02:57 1994 +0100
     1.3 @@ -236,19 +236,25 @@
     1.4  \index{tactics!for inserting facts|bold}
     1.5  \begin{ttbox} 
     1.6  cut_facts_tac : thm list -> int -> tactic
     1.7 -subgoal_tac   :   string -> int -> tactic
     1.8 +cut_inst_tac  : (string*string)list -> thm -> int -> tactic
     1.9 +subgoal_tac   : string -> int -> tactic
    1.10  \end{ttbox}
    1.11  These tactics add assumptions --- which must be proved, sooner or later ---
    1.12  to a given subgoal.
    1.13  \begin{description}
    1.14  \item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] 
    1.15    adds the {\it thms} as new assumptions to subgoal~$i$.  Once they have
    1.16 -  been inserted as assumptions, they become subject to {\tt eresolve_tac}
    1.17 -  and {\tt rewrite_goals_tac}.  Only rules with no premises are inserted:
    1.18 -  Isabelle cannot use assumptions that contain $\Imp$ or~$\Forall$.  Sometimes
    1.19 -  the theorems are premises of a rule being derived, returned by~{\tt
    1.20 -    goal}; instead of calling this tactic, you could state the goal with an
    1.21 -  outermost meta-quantifier.
    1.22 +  been inserted as assumptions, they become subject to tactics such as {\tt
    1.23 +    eresolve_tac} and {\tt rewrite_goals_tac}.  Only rules with no premises
    1.24 +  are inserted: Isabelle cannot use assumptions that contain $\Imp$
    1.25 +  or~$\Forall$.  Sometimes the theorems are premises of a rule being
    1.26 +  derived, returned by~{\tt goal}; instead of calling this tactic, you
    1.27 +  could state the goal with an outermost meta-quantifier.
    1.28 +
    1.29 +\item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
    1.30 +  instantiates the {\it thm} with the instantiations {\it insts}, as
    1.31 +  described in \S\ref{res_inst_tac}.  It adds the resulting theorem as a
    1.32 +  new assumption to subgoal~$i$. 
    1.33  
    1.34  \item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] 
    1.35  adds the {\it formula} as a assumption to subgoal~$i$, and inserts the same
    1.36 @@ -575,14 +581,16 @@
    1.37  \begin{ttbox}
    1.38  datatype 'a option = None  |  Some of 'a;
    1.39  \end{ttbox}
    1.40 +For clarity, the module name {\tt Sequence} is omitted from the signature
    1.41 +specifications below; for instance, {\tt null} appears instead of {\tt
    1.42 +  Sequence.null}.
    1.43  
    1.44  \subsubsection{Basic operations on sequences}
    1.45  \begin{ttbox} 
    1.46 -Sequence.null   : 'a Sequence.seq
    1.47 -Sequence.seqof  : (unit -> ('a * 'a Sequence.seq) option)
    1.48 -                     -> 'a Sequence.seq
    1.49 -Sequence.single : 'a -> 'a Sequence.seq
    1.50 -Sequence.pull   : 'a Sequence.seq -> ('a * 'a Sequence.seq) option
    1.51 +null   : 'a seq
    1.52 +seqof  : (unit -> ('a * 'a seq) option) -> 'a seq
    1.53 +single : 'a -> 'a seq
    1.54 +pull   : 'a seq -> ('a * 'a seq) option
    1.55  \end{ttbox}
    1.56  \begin{description}
    1.57  \item[{\tt Sequence.null}] 
    1.58 @@ -604,9 +612,9 @@
    1.59  
    1.60  \subsubsection{Converting between sequences and lists}
    1.61  \begin{ttbox} 
    1.62 -Sequence.chop: int * 'a Sequence.seq -> 'a list * 'a Sequence.seq
    1.63 -Sequence.list_of_s : 'a Sequence.seq -> 'a list
    1.64 -Sequence.s_of_list : 'a list -> 'a Sequence.seq
    1.65 +chop      : int * 'a seq -> 'a list * 'a seq
    1.66 +list_of_s : 'a seq -> 'a list
    1.67 +s_of_list : 'a list -> 'a seq
    1.68  \end{ttbox}
    1.69  \begin{description}
    1.70  \item[{\tt Sequence.chop} ($n$, $s$)] 
    1.71 @@ -624,12 +632,11 @@
    1.72  
    1.73  \subsubsection{Combining sequences}
    1.74  \begin{ttbox} 
    1.75 -Sequence.append: 'a Sequence.seq * 'a Sequence.seq -> 'a Sequence.seq
    1.76 -Sequence.interleave : 'a Sequence.seq * 'a Sequence.seq
    1.77 -                                                   -> 'a Sequence.seq
    1.78 -Sequence.flats   : 'a Sequence.seq Sequence.seq -> 'a Sequence.seq
    1.79 -Sequence.maps    : ('a -> 'b) -> 'a Sequence.seq -> 'b Sequence.seq
    1.80 -Sequence.filters : ('a -> bool) -> 'a Sequence.seq -> 'a Sequence.seq
    1.81 +append     : 'a seq * 'a seq -> 'a seq
    1.82 +interleave : 'a seq * 'a seq -> 'a seq
    1.83 +flats      : 'a seq seq -> 'a seq
    1.84 +maps       : ('a -> 'b) -> 'a seq -> 'b seq
    1.85 +filters    : ('a -> bool) -> 'a seq -> 'a seq
    1.86  \end{ttbox} 
    1.87  \begin{description}
    1.88  \item[{\tt Sequence.append} ($s@1$, $s@2$)]