# 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