--- a/doc-src/IsarRef/Thy/Spec.thy Sun Nov 28 15:34:35 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Sun Nov 28 16:15:31 2010 +0100
@@ -253,11 +253,12 @@
\begin{matharray}{rcl}
@{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "syntax_declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
\end{matharray}
\begin{rail}
- 'declaration' ('(pervasive)')? target? text
+ ('declaration' | 'syntax_declaration') ('(pervasive)')? target? text
;
'declare' target? (thmrefs + 'and')
;
@@ -275,6 +276,10 @@
declaration is applied to all possible contexts involved, including
the global background theory.
+ \item @{command "syntax_declaration"} is similar to @{command
+ "declaration"}, but is meant to affect only ``syntactic'' tools by
+ convention (such as notation and type-checking information).
+
\item @{command "declare"}~@{text thms} declares theorems to the
current local theory context. No theorem binding is involved here,
unlike @{command "theorems"} or @{command "lemmas"} (cf.\