1.1 --- a/doc-src/Ref/goals.tex	Fri Apr 22 18:08:57 1994 +0200
     1.2 +++ b/doc-src/Ref/goals.tex	Fri Apr 22 18:18:37 1994 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4  this list is non-empty, bind its value to an \ML{} identifier by typing
     1.5  something like
     1.6  \begin{ttbox} 
     1.7 -val prems = it;
     1.8 +val prems = goal{\it theory\/ formula};
     1.9  \end{ttbox}\index{assumptions!of main goal}
    1.10  These assumptions serve as the premises when you are deriving a rule.  They
    1.11  are also stored internally and can be retrieved later by the function {\tt
    1.12 @@ -53,7 +53,7 @@
    1.13  
    1.14  \index{definitions!unfolding}
    1.15  Some of the commands unfold definitions using meta-rewrite rules.  This
    1.16 -expansion affects both the first subgoal and the premises, which would
    1.17 +expansion affects both the initial subgoal and the premises, which would
    1.18  otherwise require use of {\tt rewrite_goals_tac} and
    1.19  {\tt rewrite_rule}.
    1.20  
    1.21 @@ -321,8 +321,8 @@
    1.22  
    1.23  \item[\ttindexbold{ren} {\it names} {\it i};] 
    1.24  performs \hbox{\tt by (rename_tac {\it names} {\it i});} it renames
    1.25 -parameters in subgoal~$i$.  (Ignore the message {\tt Warning:\ same as
    1.26 -previous level}.)
    1.27 +parameters in subgoal~$i$.  (Ignore the message {\footnotesize\tt Warning:\
    1.28 +  same as previous level}.)
    1.29  \index{parameters!renaming}
    1.30  \end{ttdescription}
    1.31  
    1.32 @@ -341,9 +341,9 @@
    1.33  are analogous to {\tt goal}, {\tt goalw} and {\tt goalw_cterm}.
    1.34  
    1.35  The tactic is specified by a function from theorem lists to tactic lists.
    1.36 -The function is applied to the list of meta-hypotheses taken from the main
    1.37 -goal.  The resulting tactics are applied in sequence (using {\tt EVERY}).
    1.38 -For example, a proof consisting of the commands
    1.39 +The function is applied to the list of meta-assumptions taken from
    1.40 +the main goal.  The resulting tactics are applied in sequence (using {\tt
    1.41 +  EVERY}).  For example, a proof consisting of the commands
    1.42  \begin{ttbox} 
    1.43  val prems = goal {\it theory} {\it formula};
    1.44  by \(tac@1\);  \ldots  by \(tac@n\);
    1.45 @@ -355,17 +355,10 @@
    1.46   (fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]);
    1.47  \end{ttbox}
    1.48  The methods perform identical processing of the initial {\it formula} and
    1.49 -the final proof state, but {\tt prove_goal} executes the tactic as a
    1.50 -atomic operation, bypassing the subgoal module.  
    1.51 -
    1.52 -A batch proof may alternatively consist of subgoal commands encapsulated
    1.53 -using~{\tt let}:
    1.54 -\begin{ttbox} 
    1.55 -val my_thm = 
    1.56 -    let val prems = goal {\it theory} {\it formula}
    1.57 -    in  by \(tac@1\);  \ldots  by \(tac@n\);  result() end;
    1.58 -\end{ttbox}
    1.59 -
    1.60 +the final proof state.  But {\tt prove_goal} executes the tactic as a
    1.61 +atomic operation, bypassing the subgoal module; the current interactive
    1.62 +proof is unaffected.
    1.63 +%
    1.64  \begin{ttdescription}
    1.65  \item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};] 
    1.66  executes a proof of the {\it formula\/} in the given {\it theory}, using
    1.67 @@ -429,7 +422,7 @@
    1.68  
    1.69  \item[\ttindexbold{pop_proof}();]  
    1.70  discards the top element of the stack.  It returns the list of
    1.71 -meta-hypotheses associated with the new proof;  you should bind these to an
    1.72 +assumptions associated with the new proof;  you should bind these to an
    1.73  \ML\ identifier.  They can also be obtained by calling \ttindex{premises}.
    1.74  
    1.75  \item[\ttindexbold{rotate_proof}();]