author | wenzelm |
Mon, 12 Jan 1998 17:48:55 +0100 | |
changeset 4560 | 83e1eec9cfeb |
parent 4559 | 8e604d885b54 |
child 4561 | 19f1a01570bf |
--- a/doc-src/Ref/simplifier.tex Mon Jan 12 17:48:23 1998 +0100 +++ b/doc-src/Ref/simplifier.tex Mon Jan 12 17:48:55 1998 +0100 @@ -1131,8 +1131,7 @@ fun proc _ _ (Abs _) = Some rew | proc _ _ _ = None; in - val pair_eta_expand_proc = - Simplifier.mk_simproc "pair_eta_expand" lhss proc; + val pair_eta_expand_proc = mk_simproc "pair_eta_expand" lhss proc; end; \end{ttbox} This is an example of using \texttt{pair_eta_expand_proc}: