# HG changeset patch
# User haftmann
# Date 1199433901 -3600
# Node ID 8fbc7d38d6cf9f9eebf4850eef5971cd29acb78a
# Parent  4b44d945702f7076bc2dc55870c0da5baa8050f1
fixed typo

diff -r 4b44d945702f -r 8fbc7d38d6cf doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Fri Jan 04 09:04:32 2008 +0100
+++ b/doc-src/IsarRef/syntax.tex	Fri Jan 04 09:05:01 2008 +0100
@@ -615,7 +615,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[$break = 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