# HG changeset patch
# User wenzelm
# Date 955630922 -7200
# Node ID f76f41f24c44986c0ac6cfabe846e4a84e0a65fc
# Parent  816d8f6513be7c13deef760caa86d8897f811b23
Simplifier options;

diff -r 816d8f6513be -r f76f41f24c44 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Thu Apr 13 15:01:50 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Thu Apr 13 15:02:02 2000 +0200
@@ -379,10 +379,21 @@
 \railalias{simpall}{simp\_all}
 \railterm{simpall}
 
+\railalias{noasm}{no\_asm}
+\railterm{noasm}
+
+\railalias{noasmsimp}{no\_asm\_simp}
+\railterm{noasmsimp}
+
+\railalias{noasmuse}{no\_asm\_use}
+\railterm{noasmuse}
+
 \begin{rail}
-  ('simp' | simpall) ('!' ?) (simpmod * )
+  ('simp' | simpall) ('!' ?) simpopt? (simpmod * )
   ;
 
+  simpopt: (noasm | noasmsimp | noasmuse) ':'
+  ;
   simpmod: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'other') ':' thmrefs
   ;
 \end{rail}
@@ -404,15 +415,28 @@
 \item [$simp_all$] is similar to $simp$, but acts on all goals.
 \end{descr}
 
-Internally, the $simp$ method is based on \texttt{asm_full_simp_tac}
-\cite[\S10]{isabelle-ref}, but is much better behaved in practice.  Just the
-local premises of the actual goal are involved by default.  Additional facts
-may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The
-full context of assumptions is only included in the $simp!$ version, which
-should be used with some care, though.
+By default, the Simplifier methods are based on \texttt{asm_full_simp_tac}
+internally \cite[\S10]{isabelle-ref}.  In structured proofs this is usually
+quite well behaved in practice: just the local premises of the actual goal are
+involved, additional facts may inserted via explicit forward-chaining (using
+$\THEN$, $\FROMNAME$ etc.).  The full context of assumptions is only included
+if the ``$!$'' (bang) argument is given, which should be used with some care,
+though.
 
-Note that there is no separate $split$ method.  The effect of
-\texttt{split_tac} can be simulated by $(simp~only\colon~split\colon~\vec a)$.
+Additional Simplifier options may be specified to tune the behavior even
+further: $no_asm$ means assumptions are ignored completely (cf.\ 
+\texttt{simp_tac}), $no_asm_simp$ means assumptions are used in the
+simplification of the conclusion but are not themselves simplified (cf.\ 
+\texttt{asm_simp_tac}), and $no_asm_use$ means assumptions are simplified but
+are not used in the simplification of each other or the conclusion (cf.
+\texttt{full_simp_tac}).
+
+\medskip
+
+The Splitter package is usually configured to work as part of the Simplifier.
+There is no separate $split$ method available.  The effect of repeatedly
+applying \texttt{split_tac} can be simulated by
+$(simp~only\colon~split\colon~\vec a)$.
 
 
 \subsection{Declaring rules}