--- 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}.
*}
--- 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%
%
--- 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},