# HG changeset patch
# User wenzelm
# Date 1328361914 -3600
# Node ID 7233d0521c43e401211aea8a6235590683e05684
# Parent  30953ef09bcd50d043cfe5e945773b0098efbea1
more refs;

diff -r 30953ef09bcd -r 7233d0521c43 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Feb 04 14:20:39 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Feb 04 14:25:14 2012 +0100
@@ -442,7 +442,7 @@
   line break; the entire phrase is a pretty printing block.
 
   The general idea of pretty printing with blocks and breaks is also
-  described in \cite{paulson-ml2}.
+  described in \cite{paulson-ml2}; it goes back to \cite{Oppen:1980}.
 *}
 
 
diff -r 30953ef09bcd -r 7233d0521c43 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat Feb 04 14:20:39 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat Feb 04 14:25:14 2012 +0100
@@ -561,7 +561,7 @@
   line break; the entire phrase is a pretty printing block.
 
   The general idea of pretty printing with blocks and breaks is also
-  described in \cite{paulson-ml2}.%
+  described in \cite{paulson-ml2}; it goes back to \cite{Oppen:1980}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 30953ef09bcd -r 7233d0521c43 doc-src/manual.bib
--- a/doc-src/manual.bib	Sat Feb 04 14:20:39 2012 +0100
+++ b/doc-src/manual.bib	Sat Feb 04 14:25:14 2012 +0100
@@ -1135,6 +1135,14 @@
   number =       {IC/2004/64}
 }
 
+@Article{Oppen:1980,
+  author =       {D. C. Oppen},
+  title =        {Pretty Printing},
+  journal =      {ACM Transactions on Programming Languages and Systems},
+  year =         1980,
+  volume =    2,
+  number =    4}
+
 @Manual{pvs-language,
   title		= {The {PVS} specification language},
   author	= {S. Owre and N. Shankar and J. M. Rushby},