# HG changeset patch
# User lcp
# Date 766421235 -7200
# Node ID 998f1c5adafb1e8368fe3d992f4a2770501afdcb
# Parent  76ae17549558553b3251ad36571e65f6170e1316
penultimate Springer draft

diff -r 76ae17549558 -r 998f1c5adafb doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Fri Apr 15 16:37:59 1994 +0200
+++ b/doc-src/Ref/goals.tex	Fri Apr 15 16:47:15 1994 +0200
@@ -3,9 +3,10 @@
 \index{proofs|(}
 \index{subgoal module|(}
 \index{reading!goals|see{proofs, starting}}
-The subgoal module stores the current proof state and many previous states;
-commands can produce new states or return to previous ones.  The {\em state
-list\/} at level $n$ is a list of pairs
+
+The subgoal module stores the current proof state\index{proof state} and
+many previous states; commands can produce new states or return to previous
+ones.  The {\em state list\/} at level $n$ is a list of pairs
 \[ [(\psi@n,\Psi@n),\; (\psi@{n-1},\Psi@{n-1}),\; \ldots,\; (\psi@0,[])] \]
 where $\psi@n$ is the current proof state, $\psi@{n-1}$ is the previous
 one, \ldots, and $\psi@0$ is the initial proof state.  The $\Psi@i$ are
@@ -27,7 +28,7 @@
 commands than {\tt by}, {\tt chop} and {\tt undo}.  They typically end with
 a call to {\tt result}.
 \subsection{Starting a backward proof}
-\index{proofs!starting|bold}
+\index{proofs!starting}
 \begin{ttbox} 
 goal        : theory -> string -> thm list 
 goalw       : theory -> thm list -> string -> thm list 
@@ -44,47 +45,49 @@
 something like
 \begin{ttbox} 
 val prems = it;
-\end{ttbox}
+\end{ttbox}\index{assumptions!of main goal}
 These assumptions serve as the premises when you are deriving a rule.  They
 are also stored internally and can be retrieved later by the function {\tt
-  premises}.  When the proof is finished, \ttindex{result} compares the
+  premises}.  When the proof is finished, {\tt result} compares the
 stored assumptions with the actual assumptions in the proof state.
 
+\index{definitions!unfolding}
 Some of the commands unfold definitions using meta-rewrite rules.  This
 expansion affects both the first subgoal and the premises, which would
-otherwise require use of \ttindex{rewrite_goals_tac} and
-\ttindex{rewrite_rule}.
+otherwise require use of {\tt rewrite_goals_tac} and
+{\tt rewrite_rule}.
 
-If the main goal has the form {\tt"!!{\it vars}.\ \ldots"}, with an outermost
-quantifier, then the list of premises will be empty.  Subgoal~1 will
-contain the meta-quantified {\it vars\/} as parameters and the goal's premises
-as assumptions.  This is useful when the next step of the proof would
-otherwise be to call \ttindex{cut_facts_tac} with the list of premises
-(\S\ref{cut_facts_tac}).
+\index{*"!"! symbol!in main goal}
+If the main goal has the form {\tt"!!{\it vars}.\ \ldots"}, with an
+outermost quantifier, then the list of premises will be empty.  Subgoal~1
+will contain the meta-quantified {\it vars\/} as parameters and the goal's
+premises as assumptions.  This avoids having to call
+\ttindex{cut_facts_tac} with the list of premises (\S\ref{cut_facts_tac}).
 
-\begin{description}
-\item[\ttindexbold{goal} {\it theory} {\it formula}; ] 
+\begin{ttdescription}
+\item[\ttindexbold{goal} {\it theory} {\it formula};] 
 begins a new proof, where {\it theory} is usually an \ML\ identifier
 and the {\it formula\/} is written as an \ML\ string.
 
-\item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula}; ] 
+\item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula};] 
 is like {\tt goal} but also applies the list of {\it defs\/} as
 meta-rewrite rules to the first subgoal and the premises.
-\index{rewriting!meta-level}
+\index{meta-rewriting}
 
-\item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct}; ] 
-is a version of {\tt goalw} for special applications.  The main goal is
+\item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct};] 
+is a version of {\tt goalw} for programming applications.  The main goal is
 supplied as a cterm, not as a string.  Typically, the cterm is created from
 a term~$t$ by \hbox{\tt Sign.cterm_of (sign_of thy) $t$}.
 \index{*Sign.cterm_of}\index{*sign_of}
 
 \item[\ttindexbold{premises}()] 
-returns the list of meta-hypotheses associated with the current proof, in
-case you forget to bind them to an \ML{} identifier.
-\end{description}
+returns the list of meta-hypotheses associated with the current proof (in
+case you forgot to bind them to an \ML{} identifier).
+\end{ttdescription}
+
 
 \subsection{Applying a tactic}
-\index{tactics!commands for applying|bold}
+\index{tactics!commands for applying}
 \begin{ttbox} 
 by   : tactic -> unit
 byev : tactic list -> unit
@@ -93,14 +96,14 @@
 proof state.  If the tactic succeeds, it returns a non-empty sequence of
 next states.  The head of the sequence becomes the next state, while the
 tail is retained for backtracking (see~{\tt back}).
-\begin{description} \item[\ttindexbold{by} {\it tactic}; ] 
+\begin{ttdescription} \item[\ttindexbold{by} {\it tactic};] 
 applies the {\it tactic\/} to the proof state.
 
-\item[\ttindexbold{byev} {\it tactics}; ] 
+\item[\ttindexbold{byev} {\it tactics};] 
 applies the list of {\it tactics}, one at a time.  It is useful for testing
 calls to {\tt prove_goal}, and abbreviates \hbox{\tt by (EVERY {\it
 tactics})}.
-\end{description}
+\end{ttdescription}
 
 \noindent{\it Error indications:}\nobreak
 \begin{itemize}
@@ -115,41 +118,44 @@
 \end{itemize}
 
 \subsection{Extracting the proved theorem}
-\index{ending a proof|bold}
+\index{theorems!from subgoal module}
 \begin{ttbox} 
 result  : unit -> thm
 uresult : unit -> thm
 \end{ttbox}
-\begin{description}
-\item[\ttindexbold{result}()] 
+\begin{ttdescription}
+\item[\ttindexbold{result}()]\index{assumptions!of main goal}
 returns the final theorem, after converting the free variables to
 schematics.  It discharges the assumptions supplied to the matching 
-\ttindex{goal} command.  
+{\tt goal} command.  
 
 It raises an exception unless the proof state passes certain checks.  There
-must be no assumptions other than those supplied to \ttindex{goal}.  There
+must be no assumptions other than those supplied to {\tt goal}.  There
 must be no subgoals.  The theorem proved must be a (first-order) instance
-of the original goal, as stated in the \ttindex{goal} command.  This allows
+of the original goal, as stated in the {\tt goal} command.  This allows
 {\bf answer extraction} --- instantiation of variables --- but no other
 changes to the main goal.  The theorem proved must have the same signature
 as the initial proof state.
 
-\item[\ttindexbold{uresult}()] 
-is similar but omits the checks given above.  It is needed when the initial
-goal contains function unknowns, when definitions are unfolded in the main
-goal, or when \ttindex{assume_ax} has been used.
-\end{description}
+These checks are needed because an Isabelle tactic can return any proof
+state at all.
+
+\item[\ttindexbold{uresult}()] is like {\tt result()} but omits the checks.
+  It is needed when the initial goal contains function unknowns, when
+  definitions are unfolded in the main goal (by calling
+  \ttindex{rewrite_tac}),\index{definitions!unfolding} or when
+  \ttindex{assume_ax} has been used.
+\end{ttdescription}
 
 
 \subsection{Undoing and backtracking}
-\index{backtracking command|see{\tt back}}
 \begin{ttbox} 
 chop    : unit -> unit
 choplev : int -> unit
 back    : unit -> unit
 undo    : unit -> unit
 \end{ttbox}
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{chop}();] 
 deletes the top level of the state list, cancelling the last \ttindex{by}
 command.  It provides a limited undo facility, and the {\tt undo} command
@@ -169,7 +175,7 @@
 {\tt chop}, {\tt choplev}, and~{\tt back}.  It {\bf cannot}
 cancel {\tt goal} or {\tt undo} itself.  It can be repeated to
 cancel a series of commands.
-\end{description}
+\end{ttdescription}
 
 \goodbreak
 \noindent{\it Error indications for {\tt back}:}\par\nobreak
@@ -185,13 +191,13 @@
 \end{itemize}
 
 \subsection{Printing the proof state}
-\index{printing!proof state|bold}
+\index{proof state!printing of}
 \begin{ttbox} 
 pr    : unit -> unit
 prlev : int -> unit
 goals_limit: int ref \hfill{\bf initially 10}
 \end{ttbox}
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{pr}();] 
 prints the current proof state.
 
@@ -199,123 +205,103 @@
 prints the proof state at level {\it n}.  This allows you to review the
 previous steps of the proof.
 
-\item[\ttindexbold{goals_limit} \tt:= {\it k};] 
+\item[\ttindexbold{goals_limit} := {\it k};] 
 specifies~$k$ as the maximum number of subgoals to print.
-\end{description}
+\end{ttdescription}
 
 
 \subsection{Timing}
-\index{printing!timing statistics|bold}\index{proofs!timing|bold}
+\index{timing statistics}\index{proofs!timing}
 \begin{ttbox} 
 proof_timing: bool ref \hfill{\bf initially false}
 \end{ttbox}
 
-\begin{description}
-\item[\ttindexbold{proof_timing} \tt:= true;] 
+\begin{ttdescription}
+\item[\ttindexbold{proof_timing} := true;] 
 makes the \ttindex{by} and \ttindex{prove_goal} commands display how much
 processor time was spent.  This information is compiler-dependent.
-\end{description}
+\end{ttdescription}
 
 
 \section{Shortcuts for applying tactics}
-\index{shortcuts!for ``{\tt by}'' commands|bold}
+\index{shortcuts!for {\tt by} commands}
 These commands call \ttindex{by} with common tactics.  Their chief purpose
 is to minimise typing, although the scanning shortcuts are useful in their
 own right.  Chapter~\ref{tactics} explains the tactics themselves.
 
 \subsection{Refining a given subgoal}
 \begin{ttbox} 
-ba: int -> unit
-br: thm -> int -> unit
-be: thm -> int -> unit
-bd: thm -> int -> unit
+ba  :             int -> unit
+br  : thm      -> int -> unit
+be  : thm      -> int -> unit
+bd  : thm      -> int -> unit
+brs : thm list -> int -> unit
+bes : thm list -> int -> unit
+bds : thm list -> int -> unit
 \end{ttbox}
 
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{ba} {\it i};] 
-performs \hbox{\tt by (assume_tac {\it i});}\index{*assume_tac}
+performs \hbox{\tt by (assume_tac {\it i});}
 
 \item[\ttindexbold{br} {\it thm} {\it i};] 
-performs \hbox{\tt by (resolve_tac [{\it thm}] {\it i});}\index{*resolve_tac}
+performs \hbox{\tt by (resolve_tac [{\it thm}] {\it i});}
 
 \item[\ttindexbold{be} {\it thm} {\it i};] 
-performs \hbox{\tt by (eresolve_tac [{\it thm}] {\it i});}\index{*eresolve_tac}
+performs \hbox{\tt by (eresolve_tac [{\it thm}] {\it i});}
 
 \item[\ttindexbold{bd} {\it thm} {\it i};] 
-performs \hbox{\tt by (dresolve_tac [{\it thm}] {\it i});}\index{*dresolve_tac}
-\end{description}
+performs \hbox{\tt by (dresolve_tac [{\it thm}] {\it i});}
 
-\subsubsection{Resolution with a list of theorems}
-\begin{ttbox} 
-brs: thm list -> int -> unit
-bes: thm list -> int -> unit
-bds: thm list -> int -> unit
-\end{ttbox}
-
-\begin{description}
 \item[\ttindexbold{brs} {\it thms} {\it i};] 
-performs \hbox{\tt by (resolve_tac {\it thms} {\it i});}\index{*resolve_tac}
+performs \hbox{\tt by (resolve_tac {\it thms} {\it i});}
 
 \item[\ttindexbold{bes} {\it thms} {\it i};] 
-performs \hbox{\tt by (eresolve_tac {\it thms} {\it i});}\index{*eresolve_tac}
+performs \hbox{\tt by (eresolve_tac {\it thms} {\it i});}
 
 \item[\ttindexbold{bds} {\it thms} {\it i};] 
-performs \hbox{\tt by (dresolve_tac {\it thms} {\it i});}\index{*dresolve_tac}
-\end{description}
+performs \hbox{\tt by (dresolve_tac {\it thms} {\it i});}
+\end{ttdescription}
 
 
 \subsection{Scanning shortcuts}
-\index{shortcuts!scanning for subgoals|bold}
 These shortcuts scan for a suitable subgoal (starting from subgoal~1).
 They refine the first subgoal for which the tactic succeeds.  Thus, they
 require less typing than {\tt br}, etc.  They display the selected
 subgoal's number; please watch this, for it may not be what you expect!
 
-\subsubsection{Proof by assumption and resolution}
 \begin{ttbox} 
-fa: unit -> unit
-fr: thm -> unit
-fe: thm -> unit
-fd: thm -> unit
+fa  : unit     -> unit
+fr  : thm      -> unit
+fe  : thm      -> unit
+fd  : thm      -> unit
+frs : thm list -> unit
+fes : thm list -> unit
+fds : thm list -> unit
 \end{ttbox}
 
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{fa}();] 
-solves some subgoal by assumption.\index{*assume_tac}
+solves some subgoal by assumption.
 
 \item[\ttindexbold{fr} {\it thm};] 
 refines some subgoal using \hbox{\tt resolve_tac [{\it thm}]}
-\index{*resolve_tac}
 
 \item[\ttindexbold{fe} {\it thm};] 
 refines some subgoal using \hbox{\tt eresolve_tac [{\it thm}]}
-\index{*eresolve_tac}
 
 \item[\ttindexbold{fd} {\it thm};] 
 refines some subgoal using \hbox{\tt dresolve_tac [{\it thm}]}
-\index{*dresolve_tac}
-\end{description}
 
-\subsubsection{Resolution with a list of theorems}
-\begin{ttbox} 
-frs: thm list -> unit
-fes: thm list -> unit
-fds: thm list -> unit
-\end{ttbox}
-
-\begin{description}
 \item[\ttindexbold{frs} {\it thms};] 
 refines some subgoal using \hbox{\tt resolve_tac {\it thms}}
-\index{*resolve_tac}
 
 \item[\ttindexbold{fes} {\it thms};] 
 refines some subgoal using \hbox{\tt eresolve_tac {\it thms}} 
-\index{*eresolve_tac}
 
 \item[\ttindexbold{fds} {\it thms};] 
 refines some subgoal using \hbox{\tt dresolve_tac {\it thms}} 
-\index{*dresolve_tac}
-\end{description}
+\end{ttdescription}
 
 \subsection{Other shortcuts}
 \begin{ttbox} 
@@ -323,12 +309,12 @@
 bws : thm list -> unit
 ren : string -> int -> unit
 \end{ttbox}
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{bw} {\it def};] 
 performs \hbox{\tt by (rewrite_goals_tac [{\it def}]);}
 It unfolds definitions in the subgoals (but not the main goal), by
-meta-rewriting with the given definition.\index{*rewrite_goals_tac}
-\index{rewriting!meta-level}
+meta-rewriting with the given definition.
+\index{meta-rewriting}
 
 \item[\ttindexbold{bws}] 
 is like {\tt bw} but takes a list of definitions.
@@ -337,26 +323,22 @@
 performs \hbox{\tt by (rename_tac {\it names} {\it i});} it renames
 parameters in subgoal~$i$.  (Ignore the message {\tt Warning:\ same as
 previous level}.)
-\index{*rename_tac}\index{parameters!renaming}
-\end{description}
-
+\index{parameters!renaming}
+\end{ttdescription}
 
 
-\section{Advanced features}
-\subsection{Executing batch proofs}
-\index{proofs!batch|bold}
-\index{batch execution|bold}
+\section{Executing batch proofs}
+\index{batch execution}
 \begin{ttbox}
 prove_goal  :  theory->          string->(thm list->tactic list)->thm
 prove_goalw :  theory->thm list->string->(thm list->tactic list)->thm
 prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->thm
 \end{ttbox}
-A collection of derivations may be stored for batch execution using these
-functions.  They create an initial proof state, then apply a tactic to it,
-yielding a sequence of final proof states.  The head of the sequence is
+These batch functions create an initial proof state, then apply a tactic to
+it, yielding a sequence of final proof states.  The head of the sequence is
 returned, provided it is an instance of the theorem originally proposed.
 The forms {\tt prove_goal}, {\tt prove_goalw} and {\tt prove_goalw_cterm}
-are analogous to \ttindex{goal}, \ttindex{goalw} and \ttindex{goalw_cterm}.
+are analogous to {\tt goal}, {\tt goalw} and {\tt goalw_cterm}.
 
 The tactic is specified by a function from theorem lists to tactic lists.
 The function is applied to the list of meta-hypotheses taken from the main
@@ -374,38 +356,40 @@
 \end{ttbox}
 The methods perform identical processing of the initial {\it formula} and
 the final proof state, but {\tt prove_goal} executes the tactic as a
-atomic operation, bypassing the subgoal module.  The commands can also be
-encapsulated in an expression using~{\tt let}:
+atomic operation, bypassing the subgoal module.  
+
+A batch proof may alternatively consist of subgoal commands encapsulated
+using~{\tt let}:
 \begin{ttbox} 
 val my_thm = 
     let val prems = goal {\it theory} {\it formula}
     in  by \(tac@1\);  \ldots  by \(tac@n\);  result() end;
 \end{ttbox}
 
-\begin{description}
-\item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf}; ] 
+\begin{ttdescription}
+\item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};] 
 executes a proof of the {\it formula\/} in the given {\it theory}, using
 the given tactic function.
 
 \item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula} 
-      {\it tacsf}; ]\index{rewriting!meta-level}
+      {\it tacsf};]\index{meta-rewriting}
 is like {\tt prove_goal} but also applies the list of {\it defs\/} as
 meta-rewrite rules to the first subgoal and the premises.
 
 \item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct}
-      {\it tacsf}; ] 
-is a version of {\tt prove_goalw} for special applications.  The main
+      {\it tacsf};] 
+is a version of {\tt prove_goalw} for programming applications.  The main
 goal is supplied as a cterm, not as a string.  Typically, the cterm is
 created from a term~$t$ as follows:
 \begin{ttbox}
 Sign.cterm_of (sign_of thy) \(t\)
 \end{ttbox}
 \index{*Sign.cterm_of}\index{*sign_of}
-\end{description}
+\end{ttdescription}
 
 
-\subsection{Managing multiple proofs}
-\index{proofs!managing multiple|bold}
+\section{Managing multiple proofs}
+\index{proofs!managing multiple}
 You may save the current state of the subgoal module and resume work on it
 later.  This serves two purposes.  
 \begin{enumerate}
@@ -418,27 +402,27 @@
 independently for each of the saved proofs.  In addition, each saved state
 carries a separate \ttindex{undo} list.
 
-\subsubsection{The stack of proof states}
-\index{proofs!stacking|bold}
+\subsection{The stack of proof states}
+\index{proofs!stacking}
 \begin{ttbox} 
 push_proof   : unit -> unit
 pop_proof    : unit -> thm list
 rotate_proof : unit -> thm list
 \end{ttbox}
 The subgoal module maintains a stack of proof states.  Most subgoal
-commands affect only the top of the stack.  The \ttindex{goal} command {\bf
-replaces} the top of the stack; the only command that pushes a proof on the
+commands affect only the top of the stack.  The \ttindex{goal} command {\em
+replaces\/} the top of the stack; the only command that pushes a proof on the
 stack is {\tt push_proof}.
 
 To save some point of the proof, call {\tt push_proof}.  You may now
-state a lemma using \ttindex{goal}, or simply continue to apply tactics.
+state a lemma using {\tt goal}, or simply continue to apply tactics.
 Later, you can return to the saved point by calling {\tt pop_proof} or 
 {\tt rotate_proof}. 
 
 To view the entire stack, call {\tt rotate_proof} repeatedly; as it rotates
 the stack, it prints the new top element.
 
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{push_proof}();]  
 duplicates the top element of the stack, pushing a copy of the current
 proof state on to the stack.
@@ -448,40 +432,39 @@
 meta-hypotheses associated with the new proof;  you should bind these to an
 \ML\ identifier.  They can also be obtained by calling \ttindex{premises}.
 
-\item[\ttindexbold{rotate_proof}]  
+\item[\ttindexbold{rotate_proof}();]
+\index{assumptions!of main goal}
 rotates the stack, moving the top element to the bottom.  It returns the
 list of assumptions associated with the new proof.
-\end{description}
+\end{ttdescription}
 
 
-\subsubsection{Saving and restoring proof states}
-\index{proofs!saving and restoring|bold}
+\subsection{Saving and restoring proof states}
+\index{proofs!saving and restoring}
 \begin{ttbox} 
 save_proof    : unit -> proof
 restore_proof : proof -> thm list
 \end{ttbox}
 States of the subgoal module may be saved as \ML\ values of
-type~\ttindex{proof}, and later restored.
+type~\mltydx{proof}, and later restored.
 
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{save_proof}();]  
 returns the current state, which is on top of the stack.
 
-\item[\ttindexbold{restore_proof} {\it prf}]  
-replaces the top of the stack by~{\it prf}.  It returns the list of
-assumptions associated with the new proof.
-\end{description}
+\item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal}
+  replaces the top of the stack by~{\it prf}.  It returns the list of
+  assumptions associated with the new proof.
+\end{ttdescription}
 
 
-\subsection{Debugging and inspecting}
-\index{proofs!debugging|bold}
-\index{debugging}
+\section{Debugging and inspecting}
+\index{tactics!debugging}
 These specialized operations support the debugging of tactics.  They refer
-to the current proof state of the subgoal module, and fail if there is no
-proof underway.
+to the current proof state of the subgoal module.
 
-\subsubsection{Reading and printing terms}
-\index{reading!terms|bold}\index{printing!terms}\index{printing!types}
+\subsection{Reading and printing terms}
+\index{terms!reading of}\index{terms!printing of}\index{types!printing of}
 \begin{ttbox} 
 read    : string -> term
 prin    : term -> unit
@@ -490,7 +473,7 @@
 These read and print terms (or types) using the syntax associated with the
 proof state.
 
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{read} {\it string}]  
 reads the {\it string} as a term, without type checking.
 
@@ -499,17 +482,17 @@
 
 \item[\ttindexbold{printyp} {\it T};]  
 prints the type~$T$ at the terminal.
-\end{description}
+\end{ttdescription}
 
-\subsubsection{Inspecting the proof state}
-\index{proofs!inspecting the state|bold}
+\subsection{Inspecting the proof state}
+\index{proofs!inspecting the state}
 \begin{ttbox} 
 topthm  : unit -> thm
 getgoal : int -> term
 gethyps : int -> thm list
 \end{ttbox}
 
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{topthm}()]  
 returns the proof state as an Isabelle theorem.  This is what \ttindex{by}
 would supply to a tactic at this point.  It omits the post-processing of
@@ -520,22 +503,22 @@
 this using {\tt prin}, though you may have to examine the internal
 data structure in order to locate the problem!
 
-\item[\ttindexbold{gethyps} {\it i}]  
-returns the hypotheses of subgoal~$i$ as meta-level assumptions.  In these
-theorems, the subgoal's parameters become free variables.  This command is
-supplied for debugging uses of \ttindex{METAHYPS}.
-\end{description}
+\item[\ttindexbold{gethyps} {\it i}]
+  returns the hypotheses of subgoal~$i$ as meta-level assumptions.  In
+  these theorems, the subgoal's parameters become free variables.  This
+  command is supplied for debugging uses of \ttindex{METAHYPS}.
+\end{ttdescription}
 
-\subsubsection{Filtering lists of rules}
+\subsection{Filtering lists of rules}
 \begin{ttbox} 
 filter_goal: (term*term->bool) -> thm list -> int -> thm list
 \end{ttbox}
 
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}] 
 applies \hbox{\tt filter_thms {\it could}} to subgoal~$i$ of the proof
 state and returns the list of theorems that survive the filtering. 
-\end{description}
+\end{ttdescription}
 
 \index{subgoal module|)}
 \index{proofs|)}