# HG changeset patch
# User wenzelm
# Date 1353338058 -3600
# Node ID 7ae7efef5ad8c373022212c0808d2520d54ac092
# Parent  97d2b77313a08f1abc1c23d6cd16145597257e65
more refs;

diff -r 97d2b77313a0 -r 7ae7efef5ad8 src/Doc/IsarImplementation/Eq.thy
--- a/src/Doc/IsarImplementation/Eq.thy	Sun Nov 18 19:01:30 2012 +0100
+++ b/src/Doc/IsarImplementation/Eq.thy	Mon Nov 19 16:14:18 2012 +0100
@@ -72,7 +72,12 @@
 
 section {* Conversions \label{sec:conv} *}
 
-text {* FIXME *}
+text {*
+  FIXME
+
+  The classic article that introduces the concept of conversion (for
+  Cambridge LCF) is \cite{paulson:1983}.
+*}
 
 
 section {* Rewriting \label{sec:rewriting} *}
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