49 commands may follow such a global @{command (global) "end"}, |
49 commands may follow such a global @{command (global) "end"}, |
50 although some user-interfaces might pretend that trailing input is |
50 although some user-interfaces might pretend that trailing input is |
51 admissible. |
51 admissible. |
52 |
52 |
53 @{rail " |
53 @{rail " |
54 @@{command theory} @{syntax name} imports \\ keywords? uses? @'begin' |
54 @@{command theory} @{syntax name} imports keywords? \\ @'begin' |
55 ; |
55 ; |
56 imports: @'imports' (@{syntax name} +) |
56 imports: @'imports' (@{syntax name} +) |
57 ; |
57 ; |
58 keywords: @'keywords' ((@{syntax string} +) ('::' @{syntax name} @{syntax tags})? + @'and') |
58 keywords: @'keywords' ((@{syntax string} +) ('::' @{syntax name} @{syntax tags})? + @'and') |
59 ; |
|
60 uses: @'uses' ((@{syntax name} | @{syntax parname}) +) |
|
61 "} |
59 "} |
62 |
60 |
63 \begin{description} |
61 \begin{description} |
64 |
62 |
65 \item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} |
63 \item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} |
82 @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim |
80 @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim |
83 "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations |
81 "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations |
84 with and without proof, respectively. Additional @{syntax tags} |
82 with and without proof, respectively. Additional @{syntax tags} |
85 provide defaults for document preparation (\secref{sec:tags}). |
83 provide defaults for document preparation (\secref{sec:tags}). |
86 |
84 |
87 The optional @{keyword_def "uses"} specification declares additional |
|
88 dependencies on external files (notably ML sources). Files will be |
|
89 loaded immediately (as ML), unless the name is parenthesized. The |
|
90 latter case records a dependency that needs to be resolved later in |
|
91 the text, usually via explicit @{command_ref "use"} for ML files; |
|
92 other file formats require specific load commands defined by the |
|
93 corresponding tools or packages. |
|
94 |
|
95 \item @{command (global) "end"} concludes the current theory |
85 \item @{command (global) "end"} concludes the current theory |
96 definition. Note that some other commands, e.g.\ local theory |
86 definition. Note that some other commands, e.g.\ local theory |
97 targets @{command locale} or @{command class} may involve a |
87 targets @{command locale} or @{command class} may involve a |
98 @{keyword "begin"} that needs to be matched by @{command (local) |
88 @{keyword "begin"} that needs to be matched by @{command (local) |
99 "end"}, according to the usual rules for nested blocks. |
89 "end"}, according to the usual rules for nested blocks. |