# HG changeset patch
# User haftmann
# Date 1255010355 -7200
# Node ID 9742f6130f10fc2907bf67cc17801aa644bbe557
# Parent  d403b99287ffb1970728b89ad42361ca958d44ff
corrected syntax diagrams for styles

diff -r d403b99287ff -r 9742f6130f10 doc-src/IsarRef/Thy/Document_Preparation.thy
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Oct 08 15:16:13 2009 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Oct 08 15:59:15 2009 +0200
@@ -201,9 +201,9 @@
     ;
     option: name | name '=' name
     ;
-    styles: '(' (style * ',') ')'
+    styles: '(' (style + ',') ')'
     ;
-    style: (name *)
+    style: (name +)
     ;
   \end{rail}