# HG changeset patch # User paulson # Date 843565870 -7200 # Node ID 586f3c075b05d8cc173531e114799c133d803bd4 # Parent b45d9f2042e050c9e25461f25c3a3372181e3a0f Restoration of reference to Nipkow, LICS, 1993 diff -r b45d9f2042e0 -r 586f3c075b05 doc-src/Ref/ref.bbl --- a/doc-src/Ref/ref.bbl Tue Sep 24 09:02:34 1996 +0200 +++ b/doc-src/Ref/ref.bbl Tue Sep 24 13:51:10 1996 +0200 @@ -28,6 +28,12 @@ \newblock In Mark~E. Stickel, editor, {\em 10th International Conference on Automated Deduction}, LNAI 449, pages 366--380. Springer, 1990. +\bibitem{nipkow-patterns} +Tobias Nipkow. +\newblock Functional unification of higher-order patterns. +\newblock In M.~Vardi, editor, {\em Eighth Annual Symposium on Logic in + Computer Science}, pages 64--74. {\sc ieee} Computer Society Press, 1993. + \bibitem{nipkow-prehofer} Tobias Nipkow and Christian Prehofer. \newblock Type reconstruction for type classes. diff -r b45d9f2042e0 -r 586f3c075b05 doc-src/Ref/simplifier.tex --- a/doc-src/Ref/simplifier.tex Tue Sep 24 09:02:34 1996 +0200 +++ b/doc-src/Ref/simplifier.tex Tue Sep 24 13:51:10 1996 +0200 @@ -164,7 +164,7 @@ {(\Var{i}+\Var{j})+\Var{k}}$ is ok. It will also deal gracefully with all rules whose left-hand sides are -so-called {\em higher-order patterns}~\cite{Nipkow-LICS-93}. These are terms +so-called {\em higher-order patterns}~\cite{nipkow-patterns}. These are terms in $\beta$-normal form (this will always be the case unless you have done something strange) where each occurrence of an unknown is of the form $\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are distinct bound variables.