src/Doc/ZF/ZF_Isar.thy

--- a/src/Doc/ZF/ZF_Isar.thy	Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/ZF/ZF_Isar.thy	Fri Jan 17 20:20:20 2014 +0100
@@ -67,7 +67,7 @@
     ;
     intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +)
     ;
-    hints: @{syntax (ZF) \"monos\"}? condefs? \\
+    hints: @{syntax (ZF) \"monos\"}? condefs? \<newline>
       @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
     ;
     @{syntax_def (ZF) \"monos\"}: @'monos' @{syntax thmrefs}