# HG changeset patch
# User wenzelm
# Date 1553774384 -3600
# Node ID e74444bdd310f892812b2076901b4d2ef6e097e3
# Parent  67af1c3bd36c135fba7c3acf1c418f878130ffc7
proper syntax diagrams;
tuned whitespace;

diff -r 67af1c3bd36c -r e74444bdd310 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Mar 28 12:52:31 2019 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Mar 28 12:59:44 2019 +0100
@@ -2298,7 +2298,7 @@
     @@{attribute (HOL) code} ('equation' | 'nbe' | 'abstype' | 'abstract'
       | 'del' | 'drop:' (const+) | 'abort:' (const+))?
     ;
-    @@{command (HOL) code_datatype} const+
+    @@{command (HOL) code_datatype} (const+)
     ;
     @@{attribute (HOL) code_unfold} 'del'?
     ;
@@ -2306,11 +2306,11 @@
     ;
     @@{attribute (HOL) code_abbrev} 'del'?
     ;
-    @@{command (HOL) code_thms} (const_expr+)?
+    @@{command (HOL) code_thms} (const_expr+)
     ;
-    @@{command (HOL) code_deps} (const_expr+)?
+    @@{command (HOL) code_deps} (const_expr+)
     ;
-    @@{command (HOL) code_reserved} target @{syntax string}+
+    @@{command (HOL) code_reserved} target (@{syntax string}+)
     ;
     symbol_const: @'constant' const
     ;
@@ -2318,7 +2318,7 @@
     ;
     symbol_class: @'type_class' class
     ;
-    symbol_class_relation: @'class_relation' class ( '<' | '\<subseteq>' ) class
+    symbol_class_relation: @'class_relation' class ('<' | '\<subseteq>') class
     ;
     symbol_class_instance: @'class_instance' type_constructor @'::' class
     ;