# HG changeset patch
# User wenzelm
# Date 1185648017 -7200
# Node ID 253720dddcdef588f6c7a56eccd315f4d3fe3df2
# Parent  d3873741678d4efc92291c37e5f42767d11933c3
added command 'simproc_setup', attribute "simproc";

diff -r d3873741678d -r 253720dddcde doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Fri Jul 27 22:19:49 2007 +0200
+++ b/doc-src/IsarRef/generic.tex	Sat Jul 28 20:40:17 2007 +0200
@@ -1126,6 +1126,51 @@
 \end{descr}
 
 
+\subsubsection{Simplification procedures}
+
+\indexisarcmd{simproc-setup}
+\indexisaratt{simproc}
+\begin{matharray}{rcl}
+  \isarcmd{simproc_setup} & : & \isarkeep{local{\dsh}theory} \\
+  simproc & : & \isaratt \\
+\end{matharray}
+
+\begin{rail}
+  'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
+  ;
+
+  'simproc' (('add' ':')? | 'del' ':') (name+)
+  ;
+\end{rail}
+
+\begin{descr}
+
+\item [$\isarcmd{simproc_setup}$] defines a named simplification
+  procedure that is invoked by the Simplifier whenever any of the
+  given term patterns match the current redex.  The implementation,
+  which is provided as ML source text, needs to be of type
+  \verb,morphism -> simpset -> cterm -> thm option,, where the
+  \verb,cterm, represents the current redex $r$ and the result is
+  supposed to be some proven rewrite rule $r \equiv r'$ (or a
+  generalized version), or \verb,NONE, to indicate failure.  The
+  \verb,simpset, argument holds the full context of the current
+  Simplifier invocation, including the actual Isar proof context.  The
+  \verb,morphism, informs about the difference of the original
+  compilation context wrt.\ the one of the actual application later
+  on.  The optional $\isarkeyword{identifier}$ specifies theorems that
+  represent the logical content of the abstract theory of this
+  simproc.
+
+  Morphisms and identifiers are only relevant for simprocs that are
+  defined within a local target context, e.g.\ in a locale.
+
+\item [$simproc\;add\colon\;name$ and $simproc\;del\colon\;name$] add
+  or delete named simprocs to the current Simplifier context.  The
+  default is to add a simproc.  Note that $\isarcmd{simproc_setup}$
+  already adds the new simproc to the subsequent context.
+
+\end{descr}
+
 \subsubsection{Forward simplification}
 
 \indexisaratt{simplified}