diff -r 97d2b77313a0 -r 7ae7efef5ad8 src/Doc/manual.bib
--- a/src/Doc/manual.bib	Sun Nov 18 19:01:30 2012 +0100
+++ b/src/Doc/manual.bib	Mon Nov 19 16:14:18 2012 +0100
@@ -1183,6 +1183,15 @@
   crossref	= {tlca93},
   pages		= {328-345}}
 
+@Article{paulson:1983,
+  author =       {L. C. Paulson},
+  title =        {A higher-order implementation of rewriting},
+  journal =      {Science of Computer Programming},
+  year =         1983,
+  volume =    3,
+  pages =     {119--149},
+  note =      {\url{http://www.cl.cam.ac.uk/~lp15/papers/Reports/TR035-lcp-rewriting.pdf}}}
+
 @InProceedings{paulson-CADE,
   author	= {Lawrence C. Paulson},
   title		= {A Fixedpoint Approach to Implementing (Co)Inductive