# HG changeset patch
# User wenzelm
# Date 953162822 -3600
# Node ID 70fd0b59b0e115a2aef22a5226d45f848bd8ef62
# Parent  b437907f9b2611e8661b2081541c15f5f885a21e
tuned;

diff -r b437907f9b26 -r 70fd0b59b0e1 doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Thu Mar 16 00:26:44 2000 +0100
+++ b/doc-src/IsarRef/hol.tex	Thu Mar 16 00:27:02 2000 +0100
@@ -214,8 +214,8 @@
 corresponding rules may be specified and instantiated in a casual manner.
 Furthermore, these methods provide named local contexts that may be invoked
 via the $\CASENAME$ proof command within the subsequent proof text (cf.\ 
-\S\ref{sec:proof-context}).  This accommodates compact proof texts even when
-reasoning about large specifications.
+\S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
+about large specifications.
 
 \begin{rail}
   'cases' ('simplified' ':')? term? rule?  ;
@@ -268,9 +268,9 @@
   application of the induction rule.
 \end{descr}
 
-Above methods produce named local contexts (cf.\ \S\ref{sec:proof-context}),
-as determined by the instantiated rule \emph{before} it has been applied to
-the internal proof state.\footnote{As a general principle, Isar proof text may
+Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
+determined by the instantiated rule \emph{before} it has been applied to the
+internal proof state.\footnote{As a general principle, Isar proof text may
   never refer to parts of proof states directly.} Thus proper use of symbolic
 cases usually require the rule to be instantiated fully, as far as the
 emerging local contexts and subgoals are concerned.  In particular, for
@@ -282,7 +282,7 @@
 cases present in the current proof context.
 
 
-\subsection{Augmenting the context}
+\subsection{Declaring rules}
 
 \indexisaratt{cases}\indexisaratt{induct}
 \begin{matharray}{rcl}
@@ -305,6 +305,9 @@
 declared by HOL definitional packages.  For special applications, these may be
 replaced manually by variant versions.
 
+Refer to the $case_names$ and $params$ attributes (see \S\ref{sec:cases}) to
+adjust names of cases and parameters of a rule.
+
 
 \section{Arithmetic}