equal
deleted
inserted
replaced
251 case: it consists of a theorem which is applied to the context by |
251 case: it consists of a theorem which is applied to the context by |
252 means of an attribute. |
252 means of an attribute. |
253 |
253 |
254 \begin{matharray}{rcl} |
254 \begin{matharray}{rcl} |
255 @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
255 @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
|
256 @{command_def "syntax_declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
256 @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
257 @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
257 \end{matharray} |
258 \end{matharray} |
258 |
259 |
259 \begin{rail} |
260 \begin{rail} |
260 'declaration' ('(pervasive)')? target? text |
261 ('declaration' | 'syntax_declaration') ('(pervasive)')? target? text |
261 ; |
262 ; |
262 'declare' target? (thmrefs + 'and') |
263 'declare' target? (thmrefs + 'and') |
263 ; |
264 ; |
264 \end{rail} |
265 \end{rail} |
265 |
266 |
272 the interpretation hierarchy. |
273 the interpretation hierarchy. |
273 |
274 |
274 If the @{text "(pervasive)"} option is given, the corresponding |
275 If the @{text "(pervasive)"} option is given, the corresponding |
275 declaration is applied to all possible contexts involved, including |
276 declaration is applied to all possible contexts involved, including |
276 the global background theory. |
277 the global background theory. |
|
278 |
|
279 \item @{command "syntax_declaration"} is similar to @{command |
|
280 "declaration"}, but is meant to affect only ``syntactic'' tools by |
|
281 convention (such as notation and type-checking information). |
277 |
282 |
278 \item @{command "declare"}~@{text thms} declares theorems to the |
283 \item @{command "declare"}~@{text thms} declares theorems to the |
279 current local theory context. No theorem binding is involved here, |
284 current local theory context. No theorem binding is involved here, |
280 unlike @{command "theorems"} or @{command "lemmas"} (cf.\ |
285 unlike @{command "theorems"} or @{command "lemmas"} (cf.\ |
281 \secref{sec:axms-thms}), so @{command "declare"} only has the effect |
286 \secref{sec:axms-thms}), so @{command "declare"} only has the effect |