--- 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} *}
--- 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