# HG changeset patch
# User wenzelm
# Date 953029905 -3600
# Node ID e7df316491d403f8489db9e765d532cda055dfa5
# Parent  1181723cf835f1d0dafa7be57a17b0febbba7346
tuned 'case';

diff -r 1181723cf835 -r e7df316491d4 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Tue Mar 14 11:31:04 2000 +0100
+++ b/doc-src/IsarRef/pure.tex	Tue Mar 14 11:31:45 2000 +0100
@@ -528,8 +528,8 @@
 at the current goal state, which is considered strictly non-observable in
 Isar.  Instead, the cases considered here typically emerge in a canonical way
 from certain pieces of specification that appears in the theory somewhere,
-such as an inductive definition, or recursive function.  See \S\ref{sec:FIXME}
-for more details of how this works in HOL.
+such as an inductive definition, or recursive function.  See
+\S\ref{sec:induct-method} for more details of how this works in HOL.
 
 \begin{rail}
   'fix' (vars + 'and') comment?
@@ -538,7 +538,7 @@
   ;
   'def' thmdecl? \\ var '==' term termpat? comment?
   ;
-  'case' name
+  'case' name attributes?
   ;
 
   var: name ('::' type)?
@@ -822,7 +822,7 @@
 
 \indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
 \begin{matharray}{rcl}
-  \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\
+  \NEXT & : & \isartrans{proof(state)}{proof(state)} \\
   \BG & : & \isartrans{proof(state)}{proof(state)} \\
   \EN & : & \isartrans{proof(state)}{proof(state)} \\
 \end{matharray}
@@ -831,17 +831,17 @@
 mostly handled rather casually, with little explicit user-intervention.  Any
 local goal statement automatically opens \emph{two} blocks, which are closed
 again when concluding the sub-proof (by $\QEDNAME$ etc.).  Sections of
-different context within a sub-proof may be switched via $\isarkeyword{next}$,
-which is just a single block-close followed by block-open again.  Thus the
-effect of $\isarkeyword{next}$ to reset the local proof context. There is no
-goal focus involved here!
+different context within a sub-proof may be switched via $\NEXT$, which is
+just a single block-close followed by block-open again.  Thus the effect of
+$\NEXT$ to reset the local proof context. There is no goal focus involved
+here!
 
 For slightly more advanced applications, there are explicit block parentheses
 as well.  These typically achieve a stronger forward style of reasoning.
 
 \begin{descr}
-\item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof,
-  resetting the local context to the initial one.
+\item [$\NEXT$] switches to a fresh block within a sub-proof, resetting the
+  local context to the initial one.
 \item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and
   close blocks.  Any current facts pass through ``$\isarkeyword{\{\{}$''
   unchanged, while ``$\isarkeyword{\}\}}$'' causes any result to be
@@ -855,7 +855,7 @@
 
 \section{Other commands}
 
-\subsection{Diagnostics}
+\subsection{Diagnostics}\label{sec:diag}
 
 \indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ}
 \indexisarcmd{print-facts}\indexisarcmd{print-binds}\indexisarcmd{print-cases}