1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 28 15:34:35 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 28 16:15:31 2010 +0100
     1.3 @@ -253,11 +253,12 @@
     1.4  
     1.5    \begin{matharray}{rcl}
     1.6      @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     1.7 +    @{command_def "syntax_declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     1.8      @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     1.9    \end{matharray}
    1.10  
    1.11    \begin{rail}
    1.12 -    'declaration' ('(pervasive)')? target? text
    1.13 +    ('declaration' | 'syntax_declaration') ('(pervasive)')? target? text
    1.14      ;
    1.15      'declare' target? (thmrefs + 'and')
    1.16      ;
    1.17 @@ -275,6 +276,10 @@
    1.18    declaration is applied to all possible contexts involved, including
    1.19    the global background theory.
    1.20  
    1.21 +  \item @{command "syntax_declaration"} is similar to @{command
    1.22 +  "declaration"}, but is meant to affect only ``syntactic'' tools by
    1.23 +  convention (such as notation and type-checking information).
    1.24 +
    1.25    \item @{command "declare"}~@{text thms} declares theorems to the
    1.26    current local theory context.  No theorem binding is involved here,
    1.27    unlike @{command "theorems"} or @{command "lemmas"} (cf.\

     2.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Sun Nov 28 15:34:35 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun Nov 28 16:15:31 2010 +0100
     2.3 @@ -273,11 +273,12 @@
     2.4  
     2.5    \begin{matharray}{rcl}
     2.6      \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     2.7 +    \indexdef{}{command}{syntax\_declaration}\hypertarget{command.syntax-declaration}{\hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     2.8      \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     2.9    \end{matharray}
    2.10  
    2.11    \begin{rail}
    2.12 -    'declaration' ('(pervasive)')? target? text
    2.13 +    ('declaration' | 'syntax_declaration') ('(pervasive)')? target? text
    2.14      ;
    2.15      'declare' target? (thmrefs + 'and')
    2.16      ;
    2.17 @@ -295,6 +296,9 @@
    2.18    declaration is applied to all possible contexts involved, including
    2.19    the global background theory.
    2.20  
    2.21 +  \item \hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}} is similar to \hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}, but is meant to affect only ``syntactic'' tools by
    2.22 +  convention (such as notation and type-checking information).
    2.23 +
    2.24    \item \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms} declares theorems to the
    2.25    current local theory context.  No theorem binding is involved here,
    2.26    unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\

     3.1 --- a/etc/isar-keywords-ZF.el	Sun Nov 28 15:34:35 2010 +0100
     3.2 +++ b/etc/isar-keywords-ZF.el	Sun Nov 28 16:15:31 2010 +0100
     3.3 @@ -172,6 +172,7 @@
     3.4      "subsubsect"
     3.5      "subsubsection"
     3.6      "syntax"
     3.7 +    "syntax_declaration"
     3.8      "term"
     3.9      "text"
    3.10      "text_raw"
    3.11 @@ -395,6 +396,7 @@
    3.12      "setup"
    3.13      "simproc_setup"
    3.14      "syntax"
    3.15 +    "syntax_declaration"
    3.16      "text"
    3.17      "text_raw"
    3.18      "theorems"

     4.1 --- a/etc/isar-keywords.el	Sun Nov 28 15:34:35 2010 +0100
     4.2 +++ b/etc/isar-keywords.el	Sun Nov 28 16:15:31 2010 +0100
     4.3 @@ -230,6 +230,7 @@
     4.4      "subsubsect"
     4.5      "subsubsection"
     4.6      "syntax"
     4.7 +    "syntax_declaration"
     4.8      "term"
     4.9      "termination"
    4.10      "text"
    4.11 @@ -508,6 +509,7 @@
    4.12      "sledgehammer_params"
    4.13      "statespace"
    4.14      "syntax"
    4.15 +    "syntax_declaration"
    4.16      "text"
    4.17      "text_raw"
    4.18      "theorems"

     5.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 28 15:34:35 2010 +0100
     5.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 28 16:15:31 2010 +0100
     5.3 @@ -16,7 +16,8 @@
     5.4    val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
     5.5    val add_axioms: (Attrib.binding * string) list -> theory -> theory
     5.6    val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
     5.7 -  val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
     5.8 +  val declaration: {syntax: bool, pervasive: bool} ->
     5.9 +    Symbol_Pos.text * Position.T -> local_theory -> local_theory
    5.10    val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
    5.11      local_theory -> local_theory
    5.12    val hide_class: bool -> xstring list -> theory -> theory
    5.13 @@ -180,11 +181,13 @@
    5.14  
    5.15  (* declarations *)
    5.16  
    5.17 -fun declaration pervasive (txt, pos) =
    5.18 +fun declaration {syntax, pervasive} (txt, pos) =
    5.19    ML_Lex.read pos txt
    5.20    |> ML_Context.expression pos
    5.21      "val declaration: Morphism.declaration"
    5.22 -    ("Context.map_proof (Local_Theory.declaration " ^ Bool.toString pervasive ^ " declaration)")
    5.23 +    ("Context.map_proof (Local_Theory." ^
    5.24 +      (if syntax then "syntax_declaration" else "declaration") ^ " " ^
    5.25 +      Bool.toString pervasive ^ " declaration)")
    5.26    |> Context.proof_map;
    5.27  
    5.28  

     6.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Nov 28 15:34:35 2010 +0100
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 28 16:15:31 2010 +0100
     6.3 @@ -325,8 +325,16 @@
     6.4        >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
     6.5  
     6.6  val _ =
     6.7 -  Outer_Syntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
     6.8 -    (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry Isar_Cmd.declaration);
     6.9 +  Outer_Syntax.local_theory "declaration" "generic ML declaration"
    6.10 +    (Keyword.tag_ml Keyword.thy_decl)
    6.11 +    (Parse.opt_keyword "pervasive" -- Parse.ML_source
    6.12 +      >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
    6.13 +
    6.14 +val _ =
    6.15 +  Outer_Syntax.local_theory "syntax_declaration" "generic ML declaration"
    6.16 +    (Keyword.tag_ml Keyword.thy_decl)
    6.17 +    (Parse.opt_keyword "pervasive" -- Parse.ML_source
    6.18 +      >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
    6.19  
    6.20  val _ =
    6.21    Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)