author wenzelm Wed, 07 Aug 2002 20:03:17 +0200 changeset 13474 f326c5d97d76 parent 13473 194e8d2cbe0f child 13475 459ac22f47ff
Simplifier.simproc(_i);
--- a/doc-src/Ref/simplifier.tex	Wed Aug 07 18:32:50 2002 +0200
+++ b/doc-src/Ref/simplifier.tex	Wed Aug 07 20:03:17 2002 +0200
@@ -1180,16 +1180,18 @@

\section{*Coding simplification procedures}
\begin{ttbox}
-mk_simproc: string -> cterm list ->
-              (Sign.sg -> thm list -> term -> thm option) -> simproc
+  val Simplifier.simproc: Sign.sg -> string -> string list
+    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
+  val Simplifier.simproc_i: Sign.sg -> string -> term list
+    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
\end{ttbox}

\begin{ttdescription}
-\item[\ttindexbold{mk_simproc}~$name$~$lhss$~$proc$] makes $proc$ a
-  simplification procedure for left-hand side patterns $lhss$.  The
-  name just serves as a comment.  The function $proc$ may be invoked
-  by the simplifier for redex positions matched by one of $lhss$ as
-  described below.
+\item[\ttindexbold{simproc}~$sign$~$name$~$lhss$~$proc$] makes $proc$ a
+  simplification procedure for left-hand side patterns $lhss$.  The name just
+  serves as a comment.  The function $proc$ may be invoked by the simplifier
+  for redex positions matched by one of $lhss$ as described below (which are
+  be specified as strings to be read as terms).
\end{ttdescription}

Simplification procedures are applied in a two-stage process as
@@ -1227,16 +1229,9 @@
making it rewrite only actual abstractions.  The simplification
procedure \texttt{pair_eta_expand_proc} is defined as follows:
\begin{ttbox}
-local
-  val lhss =
\begin{ttbox}