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' (@{syntax name} +) uses? @'begin' |
54 @@{command theory} @{syntax name} imports \\ keywords? uses? @'begin' |
55 ; |
55 ; |
56 |
56 imports: @'imports' (@{syntax name} +) |
|
57 ; |
|
58 keywords: @'keywords' ((@{syntax string} +) ('::' @{syntax name} @{syntax tags})? + @'and') |
|
59 ; |
57 uses: @'uses' ((@{syntax name} | @{syntax parname}) +) |
60 uses: @'uses' ((@{syntax name} | @{syntax parname}) +) |
58 "} |
61 "} |
59 |
62 |
60 \begin{description} |
63 \begin{description} |
61 |
64 |
62 \item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} |
65 \item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} |
63 starts a new theory @{text A} based on the merge of existing |
66 starts a new theory @{text A} based on the merge of existing |
64 theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}. |
67 theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}. Due to the possibility to import more |
65 |
68 than one ancestor, the resulting theory structure of an Isabelle |
66 Due to the possibility to import more than one ancestor, the |
69 session forms a directed acyclic graph (DAG). Isabelle takes care |
67 resulting theory structure of an Isabelle session forms a directed |
70 that sources contributing to the development graph are always |
68 acyclic graph (DAG). Isabelle's theory loader ensures that the |
71 up-to-date: changed files are automatically rechecked whenever a |
69 sources contributing to the development graph are always up-to-date: |
72 theory header specification is processed. |
70 changed files are automatically reloaded whenever a theory header |
73 |
71 specification is processed. |
74 The optional @{keyword_def "keywords"} specification declares outer |
|
75 syntax (\chref{ch:outer-syntax}) that is introduced in this theory |
|
76 later on (rare in end-user applications). Both minor keywords and |
|
77 major keywords of the Isar command language need to be specified, in |
|
78 order to make parsing of proof documents work properly. Command |
|
79 keywords need to be classified according to their structural role in |
|
80 the formal text. Examples may be seen in Isabelle/HOL sources |
|
81 itself, such as @{keyword "keywords"}~@{verbatim "\"typedef\""} |
|
82 @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim |
|
83 "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations |
|
84 with and without proof, respectively. Additional @{syntax tags} |
|
85 provide defaults for document preparation (\secref{sec:tags}). |
72 |
86 |
73 The optional @{keyword_def "uses"} specification declares additional |
87 The optional @{keyword_def "uses"} specification declares additional |
74 dependencies on extra files (usually ML sources). Files will be |
88 dependencies on external files (notably ML sources). Files will be |
75 loaded immediately (as ML), unless the name is parenthesized. The |
89 loaded immediately (as ML), unless the name is parenthesized. The |
76 latter case records a dependency that needs to be resolved later in |
90 latter case records a dependency that needs to be resolved later in |
77 the text, usually via explicit @{command_ref "use"} for ML files; |
91 the text, usually via explicit @{command_ref "use"} for ML files; |
78 other file formats require specific load commands defined by the |
92 other file formats require specific load commands defined by the |
79 corresponding tools or packages. |
93 corresponding tools or packages. |
80 |
94 |
81 \item @{command (global) "end"} concludes the current theory |
95 \item @{command (global) "end"} concludes the current theory |
82 definition. Note that local theory targets involve a local |
96 definition. Note that some other commands, e.g.\ local theory |
83 @{command (local) "end"}, which is clear from the nesting. |
97 targets @{command locale} or @{command class} may involve a |
|
98 @{keyword "begin"} that needs to be matched by @{command (local) |
|
99 "end"}, according to the usual rules for nested blocks. |
84 |
100 |
85 \end{description} |
101 \end{description} |
86 *} |
102 *} |
87 |
103 |
88 |
104 |