
diff -r 36865f14e5ce -r 7f18f5ffbb92 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Thu Oct 21 17:42:42 1999 +0200
+++ b/doc-src/IsarRef/generic.tex	Thu Oct 21 18:04:07 1999 +0200
@@ -29,29 +29,30 @@
   plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
   $\PROOFNAME$ alone.
 \item [$assumption$] solves some goal by assumption.  Any facts given are
-  guaranteed to participate in the refinement.
+  guaranteed to participate in the refinement.  Note that ``$\DOT$'' (dot)
+  abbreviates $\BY{assumption}$.
 \item [$rule~thms$] applies some rule given as argument in backward manner;
   facts are used to reduce the rule before applying it to the goal.  Thus
   $rule$ without facts is plain \emph{introduction}, while with facts it
-  becomes an \emph{elimination}.
+  becomes a (generalized) \emph{elimination}.
   
   Note that the classical reasoner introduces another version of $rule$ that
   is able to pick appropriate rules automatically, whenever explicit $thms$
   are omitted (see \S\ref{sec:classical-basic}); that method is the default
-  one for initial proof steps, such as $\PROOFNAME$ and ``$\DDOT$'' (two
-  dots).
+  for $\PROOFNAME$ steps.  Note that ``$\DDOT$'' (double-dot) abbreviates
+  $\BY{default}$.
 \item [$erule~thms$] is similar to $rule$, but applies rules by
   elim-resolution.  This is an improper method, mainly for experimentation and
   porting of old scripts.  Actual elimination proofs are usually done with
-  $rule$ (single step, involving facts) or $elim$ (multiple steps, see
+  $rule$ (single step, involving facts) or $elim$ (repeated steps, see
   \S\ref{sec:classical-basic}).
 \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
   meta-level definitions throughout all goals; any facts provided are
   \emph{ignored}.
 \item [$succeed$] yields a single (unchanged) result; it is the identify of
-  the ``\texttt{,}'' method combinator.
+  the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
 \item [$fail$] yields an empty result sequence; it is the identify of the
-  ``\texttt{|}'' method combinator.
+  ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
 \end{descr}
 
 
@@ -91,9 +92,9 @@
 \end{rail}
 
 \begin{descr}
-\item [$tag~tags$ and $untag~tags$] add and remove $tags$ to the theorem,
+\item [$tag~tags$ and $untag~tags$] add and remove $tags$ of the theorem,
   respectively.  Tags may be any list of strings that serve as comment for
-  some tools (e.g.\ $\LEMMANAME$ causes tag ``$lemma$'' to be added to the
+  some tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
   result).
 \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
   $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
@@ -102,8 +103,7 @@
   
   $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$
   that does not include the automatic lifting process that is normally
-  intended (see also \texttt{RS} and \texttt{COMP} in
-  \cite[\S5]{isabelle-ref}).
+  intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).
   
 \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
   instantiation, respectively.  The terms given in $of$ are substituted for
@@ -113,7 +113,8 @@
 \item [$standard$] puts a theorem into the standard form of object-rules, just
   as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
   
-\item [$elimify$] turns an destruction rule into an elimination.
+\item [$elimify$] turns an destruction rule into an elimination, just as the
+  ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
   
 \item [$export$] lifts a local result out of the current proof context,
   generalizing all fixed variables and discharging all assumptions.  Note that
@@ -139,12 +140,12 @@
 Calculational proof is forward reasoning with implicit application of
 transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
 an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
-results obtained by transitivity obtained together with the current result.
-Command $\ALSO$ updates $calculation$ from the most recent result, while
-$\FINALLY$ exhibits the final result by forward chaining towards the next goal
-statement.  Both commands require valid current facts, i.e.\ may occur only
-after commands that produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or
-some finished $\HAVENAME$ or $\SHOWNAME$.
+results obtained by transitivity composed with the current result.  Command
+$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
+final $calculation$ by forward chaining towards the next goal statement.  Both
+commands require valid current facts, i.e.\ may occur only after commands that
+produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
+$\HAVENAME$, $\SHOWNAME$ etc.
 
 Also note that the automatic term abbreviation ``$\dots$'' has its canonical
 application with calculational proofs.  It automatically refers to the
@@ -179,17 +180,19 @@
 \item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
   $\ALSO$, and concludes the current calculational thread.  The final result
   is exhibited as fact for forward chaining towards the next goal. Basically,
-  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  A typical proof
-  idiom is ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$''.
+  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Typical proof
+  idioms are``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
+  ``$\FINALLY~\HAVE{}{\phi}~\DOT$''.
   
 \item [$trans$] maintains the set of transitivity rules of the theory or proof
   context, by adding or deleting theorems (the default is to add).
 \end{descr}
 
-See theory \texttt{HOL/Isar_examples/Group} for a simple application of
-calculations for basic equational reasoning.
-\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
-calculational steps in combination with natural deduction.
+%FIXME
+%See theory \texttt{HOL/Isar_examples/Group} for a simple application of
+%calculations for basic equational reasoning.
+%\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
+%calculational steps in combination with natural deduction.
 
 
 \section{Axiomatic Type Classes}\label{sec:axclass}
@@ -231,7 +234,7 @@
   establish the characteristic theorems of the type classes involved.  After
   finishing the proof the theory will be augmented by a type signature
   declaration corresponding to the resulting theorem.
-\item [$intro_classes$] iteratively expands the class introduction rules of
+\item [$intro_classes$] repeatedly expands the class introduction rules of
   this theory.
 \end{descr}
 
@@ -243,17 +246,13 @@
 
 \subsection{Simplification methods}\label{sec:simp}
 
-\indexisarmeth{simp}\indexisarmeth{asm-simp}
+\indexisarmeth{simp}
 \begin{matharray}{rcl}
   simp & : & \isarmeth \\
-  asm_simp & : & \isarmeth \\
 \end{matharray}
 
-\railalias{asmsimp}{asm\_simp}
-\railterm{asmsimp}
-
 \begin{rail}
-  ('simp' | asmsimp) (simpmod * )
+  'simp' (simpmod * )
   ;
 
   simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
@@ -261,15 +260,20 @@
 \end{rail}
 
 \begin{descr}
-\item [$simp$ and $asm_simp$] invoke Isabelle's simplifier, after modifying
-  the context by adding or deleting given rules.  The \railtoken{only}
-  modifier first removes all other rewrite rules and congruences, and then is
-  like \railtoken{add}.  In contrast, \railtoken{other} ignores its arguments;
+\item [$simp$] invokes Isabelle's simplifier, after modifying the context by
+  adding or deleting rules as specified.  The \railtoken{only} modifier first
+  removes all other rewrite rules and congruences, and then is like
+  \railtoken{add}.  In contrast, \railtoken{other} ignores its arguments;
   nevertheless there may be side-effects on the context via attributes.  This
   provides a back door for arbitrary context manipulation.
   
-  Both of these methods are based on \texttt{asm_full_simp_tac}, see
-  \cite[\S10]{isabelle-ref}; $simp$ removes any premises of the goal, before
+  The $simp$ method is based on \texttt{asm_full_simp_tac} (see also
+  \cite[\S10]{isabelle-ref}), but is much better behaved in practice.  Only
+  the local premises of the actual goal are involved by default.  Additional
+  facts may be insert via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).
+  The full context of assumptions is
+
+; $simp$ removes any premises of the goal, before
   inserting the goal facts; $asm_simp$ leaves the premises.  Thus $asm_simp$
   may refer to premises that are not explicitly spelled out, potentially
   obscuring the reasoning.  The plain $simp$ method is more faithful in the




