# HG changeset patch
# User wenzelm
# Date 1553773755 -3600
# Node ID 90692c3d5ba29a00f6676a61170c614506d7b69d
# Parent  0addec5ab4adf9f0e08cf6126db6533155eb6339
tuned whitespace;

diff -r 0addec5ab4ad -r 90692c3d5ba2 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Mar 28 12:39:34 2019 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Mar 28 12:49:15 2019 +0100
@@ -2281,13 +2281,13 @@
   \end{matharray}
 
   \<^rail>\<open>
-    @@{command (HOL) export_code} ( @'open' ) ? ( constexpr + ) \<newline>
-       ( ( @'in' target ( @'module_name' @{syntax string} ) ? \<newline>
-        ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ?
+    @@{command (HOL) export_code} @'open'? (constexpr+) \<newline>
+       ((@'in' target (@'module_name' @{syntax string})? \<newline>
+        (@'file' @{syntax string})? ('(' args ')')?)+) ?
     ;
     const: @{syntax term}
     ;
-    constexpr: ( const | 'name._' | '_' )
+    constexpr: (const | 'name._' | '_')
     ;
     typeconstructor: @{syntax name}
     ;
@@ -2295,78 +2295,77 @@
     ;
     target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
     ;
-    @@{attribute (HOL) code} ( 'equation' | 'nbe' | 'abstype' | 'abstract'
-      | 'del' | 'drop:' ( const + ) | 'abort:' ( const + ) )?
+    @@{attribute (HOL) code} ('equation' | 'nbe' | 'abstype' | 'abstract'
+      | 'del' | 'drop:' (const+) | 'abort:' (const+))?
     ;
-    @@{command (HOL) code_datatype} ( const + )
-    ;
-    @@{attribute (HOL) code_unfold} ( 'del' ) ?
+    @@{command (HOL) code_datatype} const+
     ;
-    @@{attribute (HOL) code_post} ( 'del' ) ?
+    @@{attribute (HOL) code_unfold} 'del'?
     ;
-    @@{attribute (HOL) code_abbrev} ( 'del' ) ?
+    @@{attribute (HOL) code_post} 'del'?
     ;
-    @@{command (HOL) code_thms} ( constexpr + ) ?
+    @@{attribute (HOL) code_abbrev} 'del'?
     ;
-    @@{command (HOL) code_deps} ( constexpr + ) ?
+    @@{command (HOL) code_thms} (constexpr+)?
     ;
-    @@{command (HOL) code_reserved} target ( @{syntax string} + )
+    @@{command (HOL) code_deps} (constexpr+)?
     ;
-    symbol_const: ( @'constant' const )
+    @@{command (HOL) code_reserved} target @{syntax string}+
     ;
-    symbol_typeconstructor: ( @'type_constructor' typeconstructor )
+    symbol_const: @'constant' const
     ;
-    symbol_class: ( @'type_class' class )
+    symbol_typeconstructor: @'type_constructor' typeconstructor
     ;
-    symbol_class_relation: ( @'class_relation' class ( '<' | '\<subseteq>' ) class )
+    symbol_class: @'type_class' class
     ;
-    symbol_class_instance: ( @'class_instance' typeconstructor @'::' class )
+    symbol_class_relation: @'class_relation' class ( '<' | '\<subseteq>' ) class
     ;
-    symbol_module: ( @'code_module' name )
+    symbol_class_instance: @'class_instance' typeconstructor @'::' class
     ;
-    syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
+    symbol_module: @'code_module' name
     ;
-    printing_const: symbol_const ( '\<rightharpoonup>' | '=>' ) \<newline>
-      ( '(' target ')' syntax ? + @'and' )
+    syntax: @{syntax string} | (@'infix' | @'infixl' | @'infixr')
+      @{syntax nat} @{syntax string}
     ;
-    printing_typeconstructor: symbol_typeconstructor ( '\<rightharpoonup>' | '=>' ) \<newline>
-      ( '(' target ')' syntax ? + @'and' )
+    printing_const: symbol_const ('\<rightharpoonup>' | '=>') \<newline>
+      ('(' target ')' syntax ? + @'and')
     ;
-    printing_class: symbol_class ( '\<rightharpoonup>' | '=>' ) \<newline>
-      ( '(' target ')' @{syntax string} ? + @'and' )
+    printing_typeconstructor: symbol_typeconstructor ('\<rightharpoonup>' | '=>') \<newline>
+      ('(' target ')' syntax ? + @'and')
     ;
-    printing_class_relation: symbol_class_relation ( '\<rightharpoonup>' | '=>' ) \<newline>
-      ( '(' target ')' @{syntax string} ? + @'and' )
+    printing_class: symbol_class ('\<rightharpoonup>' | '=>') \<newline>
+      ('(' target ')' @{syntax string} ? + @'and')
     ;
-    printing_class_instance: symbol_class_instance ( '\<rightharpoonup>' | '=>' ) \<newline>
-      ( '(' target ')' '-' ? + @'and' )
+    printing_class_relation: symbol_class_relation ('\<rightharpoonup>' | '=>') \<newline>
+      ('(' target ')' @{syntax string} ? + @'and')
     ;
-    printing_module: symbol_module ( '\<rightharpoonup>' | '=>' ) \<newline>
-      ( '(' target ')' \<newline>
-        ( @{syntax string}
-          ( @'for' (
-            ( symbol_const | symbol_typeconstructor | symbol_class | symbol_class_relation | symbol_class_instance ) + )
-          ) ? ) ? + @'and' )
+    printing_class_instance: symbol_class_instance ('\<rightharpoonup>'| '=>') \<newline>
+      ('(' target ')' '-' ? + @'and')
+    ;
+    printing_module: symbol_module ('\<rightharpoonup>' | '=>') \<newline>
+      ('(' target ')' \<newline>
+        (@{syntax string}
+          (@'for' ((symbol_const | symbol_typeconstructor | symbol_class | symbol_class_relation | symbol_class_instance)+))?)? + @'and')
     ;
-    @@{command (HOL) code_printing} ( ( printing_const | printing_typeconstructor
+    @@{command (HOL) code_printing} ((printing_const | printing_typeconstructor
       | printing_class | printing_class_relation | printing_class_instance
-      | printing_module ) + '|' )
+      | printing_module) + '|')
     ;
-    @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor
+    @@{command (HOL) code_identifier} ((symbol_const | symbol_typeconstructor
       | symbol_class | symbol_class_relation | symbol_class_instance
-      | symbol_module ) ( '\<rightharpoonup>' | '=>' ) \<newline>
-      ( '(' target ')' @{syntax string} ? + @'and' ) + '|' )
+      | symbol_module ) ('\<rightharpoonup>' | '=>') \<newline>
+      ('(' target ')' @{syntax string} ? + @'and') + '|')
     ;
     @@{command (HOL) code_monad} const const target
     ;
     @@{command (HOL) code_reflect} @{syntax string} \<newline>
-      ( @'datatypes' ( @{syntax string} '=' ( '_' | ( @{syntax string} + '|' ) + @'and' ) ) ) ? \<newline>
-      ( @'functions' ( @{syntax string} + ) ) ? ( @'file' @{syntax string} ) ?
+      (@'datatypes' (@{syntax string} '=' ('_' | (@{syntax string} + '|') + @'and')))? \<newline>
+      (@'functions' (@{syntax string} +))? (@'file' @{syntax string})?
     ;
     @@{command (HOL) code_pred} \<newline> ('(' @'modes' ':' modedecl ')')? \<newline> const
     ;
     modedecl: (modes | ((const ':' modes) \<newline>
-        (@'and' ((const ':' modes @'and') +))?))
+      (@'and' ((const ':' modes @'and')+))?))
     ;
     modes: mode @'as' const
   \<close>