summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 07 Aug 2002 20:11:07 +0200 | |

changeset 13477 | 6f9111705d4f |

parent 13476 | 600f1c93124f |

child 13478 | 9cfbcb9acfef |

tuned;

--- a/doc-src/Ref/simplifier.tex Wed Aug 07 20:05:43 2002 +0200 +++ b/doc-src/Ref/simplifier.tex Wed Aug 07 20:11:07 2002 +0200 @@ -1187,11 +1187,14 @@ \end{ttbox} \begin{ttdescription} -\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). +\item[\ttindexbold{Simplifier.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). + +\item[\ttindexbold{Simplifier.simproc_i}] is similar to + \verb,Simplifier.simproc,, but takes well-typed terms as pattern argument. \end{ttdescription} Simplification procedures are applied in a two-stage process as @@ -1230,8 +1233,11 @@ procedure \texttt{pair_eta_expand_proc} is defined as follows: \begin{ttbox} val pair_eta_expand_proc = - Simplifier.simproc (Theory.sign_of (the_context ())) "pair_eta_expand" ["f::'a*'b=>'c"] - (fn _ => fn _ => fn t => case t of Abs _ => Some (mk_meta_eq pair_eta_expand) | _ => None); + Simplifier.simproc (Theory.sign_of (the_context ())) + "pair_eta_expand" ["f::'a*'b=>'c"] + (fn _ => fn _ => fn t => + case t of Abs _ => Some (mk_meta_eq pair_eta_expand) + | _ => None); \end{ttbox} This is an example of using \texttt{pair_eta_expand_proc}: \begin{ttbox}