
diff -r f27cc0a43feb -r 8b2eb3b78cc3 doc-src/IsarRef/conversion.tex
--- a/doc-src/IsarRef/conversion.tex	Fri Mar 08 15:33:32 2002 +0100
+++ b/doc-src/IsarRef/conversion.tex	Fri Mar 08 15:53:15 2002 +0100
@@ -1,5 +1,5 @@
 
-\chapter{Isabelle/Isar Conversion Guide}\label{ap:conv}
+\chapter{Isabelle/Isar conversion guide}\label{ap:conv}
 
 Subsequently, we give a few practical hints on working in a mixed environment
 of old Isabelle ML proof scripts and new Isabelle/Isar theories.  There are
@@ -39,21 +39,21 @@
 \begin{descr}
 \item [$\mathtt{thm}~name$ and $\mathtt{thms}~name$] retrieve theorems stored
   in the current theory context, including any ancestor node.
-  
+
   The convention of old-style theories was to bind any theorem as an ML value
   as well.  New-style theories no longer do this, so ML code may require
   \texttt{thm~"foo"} rather than just \texttt{foo}.
-  
+
 \item [$\mathtt{the_context()}$] refers to the current theory context.
-  
+
   Old-style theories often use the ML binding \texttt{thy}, which is
   dynamically created by the ML code generated from old theory source.  This
   is no longer the recommended way in any case!  Function \texttt{the_context}
   should be used for old scripts as well.
-  
+
 \item [$\mathtt{theory}~name$] retrieves the named theory from the global
   theory-loader database.
-  
+
   The ML code generated from old-style theories would include an ML binding
   $name\mathtt{.thy}$ as part of an ML structure.
 \end{descr}
@@ -72,11 +72,11 @@
 these later.
 
 \begin{descr}
-  
+
 \item [$\mathtt{qed}~name$] is the canonical way to conclude a proof script in
   ML.  This already manages entry in the theorem database of the current
   theory context.
-  
+
 \item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$]
   store theorems that have been produced in ML in an ad-hoc manner.
 
@@ -133,13 +133,13 @@
 \item Quoted strings may contain arbitrary white space, and span several lines
   without requiring \verb,\,\,\dots\verb,\, escapes.
 \item Names may always be quoted.
-  
+
   The old syntax would occasionally demand plain identifiers vs.\ quoted
   strings to accommodate certain syntactic features.
 \item Types and terms have to be \emph{atomic} as far as the theory syntax is
   concerned; this typically requires quoting of input strings, e.g.\ ``$x +
   y$''.
-  
+
   The old theory syntax used to fake part of the syntax of types in order to
   require less quoting in common cases; this was hard to predict, though.  On
   the other hand, Isar does not require quotes for simple terms, such as plain
@@ -300,12 +300,12 @@
 rule applications (based on higher-order resolution).  The space of resolution
 tactics has the following main dimensions.
 \begin{enumerate}
-\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\ 
+\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\
   \texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac},
   \texttt{forward_tac}).
-\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\ 
+\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\
   \texttt{res_inst_tac}).
-\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\ 
+\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\
   \texttt{rtac}).
 \end{enumerate}
 
@@ -348,9 +348,9 @@
 
 The main Simplifier tactics \texttt{Simp_tac}, \texttt{simp_tac} and variants
 (cf.\ \cite{isabelle-ref}) are all covered by the $simp$ and $simp_all$
-methods (see \S\ref{sec:simp}).  Note that there is no individual goal
-addressing available, simplification acts either on the first goal ($simp$)
-or all goals ($simp_all$).
+methods (see \S\ref{sec:simplifier}).  Note that there is no individual goal
+addressing available, simplification acts either on the first goal ($simp$) or
+all goals ($simp_all$).
 
 \begin{matharray}{lll}
   \texttt{Asm_full_simp_tac 1} & & simp \\
@@ -361,8 +361,9 @@
 \end{matharray}
 
 Isar also provides separate method modifier syntax for augmenting the
-Simplifier context (see \S\ref{sec:simp}), which is known as the ``simpset''
-in ML.  A typical ML expression with simpset changes looks like this:
+Simplifier context (see \S\ref{sec:simplifier}), which is known as the
+``simpset'' in ML.  A typical ML expression with simpset changes looks like
+this:
 \begin{ttbox}
 asm_full_simp_tac (simpset () addsimps [\(a@1\), \(\dots\)] delsimps [\(b@1\), \(\dots\)]) 1
 \end{ttbox}
@@ -380,7 +381,7 @@
 automated tactics, such as \texttt{Blast_tac}, \texttt{Fast_tac},
 \texttt{Clarify_tac} etc.\ (see \cite{isabelle-ref}).  The corresponding Isar
 methods usually share the same base name, such as $blast$, $fast$, $clarify$
-etc.\ (see \S\ref{sec:classical-auto}).
+etc.\ (see \S\ref{sec:classical}).
 
 Similar to the Simplifier, there is separate method modifier syntax for
 augmenting the Classical Reasoner context, which is known as the ``claset'' in
@@ -442,14 +443,13 @@
 \medskip \texttt{ALLGOALS}, \texttt{SOMEGOAL} etc.\ (see \cite{isabelle-ref})
 are not available in Isar, since there is no direct goal addressing.
 Nevertheless, some basic methods address all goals internally, notably
-$simp_all$ (see \S\ref{sec:simp}).  Also note that \texttt{ALLGOALS} may be
-often replaced by ``$+$'' (repeat at least once), although this usually has a
-different operational behavior, such as solving goals in a different order.
+$simp_all$ (see \S\ref{sec:simplifier}).  Also note that \texttt{ALLGOALS} may
+be often replaced by ``$+$'' (repeat at least once), although this usually has
+a different operational behavior, such as solving goals in a different order.
 
 \medskip Iterated resolution, such as
 \texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed
-using the $intro$ and $elim$ methods of Isar (see
-\S\ref{sec:classical-basic}).
+using the $intro$ and $elim$ methods of Isar (see \S\ref{sec:classical}).
 
 
 \subsection{Declarations and ad-hoc operations}\label{sec:conv-decls}
@@ -559,8 +559,7 @@
 machine-checked formal proof.  Depending on the context of application, this
 might be even indispensable to start with!
 
-
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "isar-ref"
-%%% End: 
+%%% End:




