# HG changeset patch
# User wenzelm
# Date 1083441532 -7200
# Node ID eafb91eda9e844ec839d33b7e18c2ab13c2203fa
# Parent  edb7dacde656fbb230653b33f53ccd6bc729d078
breaks flag;

diff -r edb7dacde656 -r eafb91eda9e8 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Thu Apr 29 06:05:03 2004 +0200
+++ b/doc-src/IsarRef/syntax.tex	Sat May 01 21:58:52 2004 +0200
@@ -522,6 +522,7 @@
 \item[$display = bool$] indicates if the text is to be output as multi-line
   ``display material'', rather than a small piece of text without line breaks
   (which is the default).
+\item[$breaks = bool$] controls line breaks in non-display material.
 \item[$quotes = bool$] indicates if the output should be enclosed in double
   quotes.
 \item[$mode = name$] adds $name$ to the print mode to be used for presentation