--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Mar 28 12:59:44 2019 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Mar 28 13:06:32 2019 +0100
@@ -2281,20 +2281,22 @@
\end{matharray}
\<^rail>\<open>
- @@{command (HOL) export_code} @'open'? (const_expr+) \<newline>
- ((@'in' target (@'module_name' @{syntax string})? \<newline>
- (@'file' @{syntax string})? ('(' args ')')?)+) ?
+ @@{command (HOL) export_code} @'open'? \<newline> (const_expr+) (export_target*)
+ ;
+ export_target:
+ @'in' target (@'module_name' @{syntax string})? \<newline>
+ (@'file' @{syntax string})? ('(' args ')')?
+ ;
+ target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
+ ;
+ const_expr: (const | 'name._' | '_')
;
const: @{syntax term}
;
- const_expr: (const | 'name._' | '_')
- ;
type_constructor: @{syntax name}
;
class: @{syntax name}
;
- target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
- ;
@@{attribute (HOL) code} ('equation' | 'nbe' | 'abstype' | 'abstract'
| 'del' | 'drop:' (const+) | 'abort:' (const+))?
;