updated generated files;
authorwenzelm
Mon Mar 01 17:12:43 2010 +0100 (2010-03-01)
changeset 35414cc8e4276d093
parent 35413 4c7cba1f7ce9
child 35420 70395c8e8c07
updated generated files;
doc-src/IsarImplementation/Thy/document/Prelim.tex
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
etc/isar-keywords-ZF.el
etc/isar-keywords.el
     1.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Mon Mar 01 17:09:42 2010 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Mon Mar 01 17:12:43 2010 +0100
     1.3 @@ -544,14 +544,14 @@
     1.4  \ \ \ \ val\ empty\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
     1.5  \ \ \ \ val\ extend\ {\isacharequal}\ I{\isacharsemicolon}\isanewline
     1.6  \ \ \ \ fun\ merge\ {\isacharparenleft}ts{\isadigit{1}}{\isacharcomma}\ ts{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\isanewline
     1.7 -\ \ \ \ \ \ OrdList{\isachardot}union\ TermOrd{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isacharsemicolon}\isanewline
     1.8 +\ \ \ \ \ \ OrdList{\isachardot}union\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isacharsemicolon}\isanewline
     1.9  \ \ {\isacharparenright}\isanewline
    1.10  \isanewline
    1.11  \ \ val\ get\ {\isacharequal}\ Terms{\isachardot}get{\isacharsemicolon}\isanewline
    1.12  \isanewline
    1.13  \ \ fun\ add\ raw{\isacharunderscore}t\ thy\ {\isacharequal}\isanewline
    1.14  \ \ \ \ let\ val\ t\ {\isacharequal}\ Sign{\isachardot}cert{\isacharunderscore}term\ thy\ raw{\isacharunderscore}t\isanewline
    1.15 -\ \ \ \ in\ Terms{\isachardot}map\ {\isacharparenleft}OrdList{\isachardot}insert\ TermOrd{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ t{\isacharparenright}\ thy\ end{\isacharsemicolon}\isanewline
    1.16 +\ \ \ \ in\ Terms{\isachardot}map\ {\isacharparenleft}OrdList{\isachardot}insert\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ t{\isacharparenright}\ thy\ end{\isacharsemicolon}\isanewline
    1.17  \isanewline
    1.18  \ \ end{\isacharsemicolon}\isanewline
    1.19  {\isacharverbatimclose}%
     2.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Mon Mar 01 17:09:42 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Mon Mar 01 17:12:43 2010 +0100
     2.3 @@ -378,34 +378,47 @@
     2.4  \end{isamarkuptext}%
     2.5  \isamarkuptrue%
     2.6  %
     2.7 -\isamarkupsection{Explicit term notation%
     2.8 +\isamarkupsection{Explicit notation%
     2.9  }
    2.10  \isamarkuptrue%
    2.11  %
    2.12  \begin{isamarkuptext}%
    2.13  \begin{matharray}{rcll}
    2.14 +    \indexdef{}{command}{type\_notation}\hypertarget{command.type-notation}{\hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    2.15 +    \indexdef{}{command}{no\_type\_notation}\hypertarget{command.no-type-notation}{\hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}type{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    2.16      \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    2.17      \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    2.18    \end{matharray}
    2.19  
    2.20    \begin{rail}
    2.21 +    ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
    2.22 +    ;
    2.23      ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
    2.24      ;
    2.25    \end{rail}
    2.26  
    2.27    \begin{description}
    2.28  
    2.29 +  \item \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix
    2.30 +  syntax with an existing type constructor.  The arity of the
    2.31 +  constructor is retrieved from the context.
    2.32 +  
    2.33 +  \item \hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}type{\isacharunderscore}notation}}}} is similar to \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}, but removes the specified syntax annotation from
    2.34 +  the present context.
    2.35 +
    2.36    \item \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix
    2.37 -  syntax with an existing constant or fixed variable.  This is a
    2.38 -  robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive
    2.39 -  (\secref{sec:syn-trans}).  Type declaration and internal syntactic
    2.40 -  representation of the given entity is retrieved from the context.
    2.41 +  syntax with an existing constant or fixed variable.  The type
    2.42 +  declaration of the given entity is retrieved from the context.
    2.43    
    2.44    \item \hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}},
    2.45    but removes the specified syntax annotation from the present
    2.46    context.
    2.47  
    2.48 -  \end{description}%
    2.49 +  \end{description}
    2.50 +
    2.51 +  Compared to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}} primitives (\secref{sec:syn-trans}), the above commands
    2.52 +  provide explicit checking wrt.\ the logical context, and work within
    2.53 +  general local theory targets, not just the global theory.%
    2.54  \end{isamarkuptext}%
    2.55  \isamarkuptrue%
    2.56  %
     3.1 --- a/etc/isar-keywords-ZF.el	Mon Mar 01 17:09:42 2010 +0100
     3.2 +++ b/etc/isar-keywords-ZF.el	Mon Mar 01 17:12:43 2010 +0100
     3.3 @@ -30,7 +30,6 @@
     3.4      "arities"
     3.5      "assume"
     3.6      "attribute_setup"
     3.7 -    "axclass"
     3.8      "axiomatization"
     3.9      "axioms"
    3.10      "back"
    3.11 @@ -108,6 +107,7 @@
    3.12      "no_notation"
    3.13      "no_syntax"
    3.14      "no_translations"
    3.15 +    "no_type_notation"
    3.16      "nonterminals"
    3.17      "notation"
    3.18      "note"
    3.19 @@ -189,6 +189,7 @@
    3.20      "txt"
    3.21      "txt_raw"
    3.22      "typ"
    3.23 +    "type_notation"
    3.24      "typed_print_translation"
    3.25      "typedecl"
    3.26      "types"
    3.27 @@ -348,7 +349,6 @@
    3.28      "abbreviation"
    3.29      "arities"
    3.30      "attribute_setup"
    3.31 -    "axclass"
    3.32      "axiomatization"
    3.33      "axioms"
    3.34      "class"
    3.35 @@ -385,6 +385,7 @@
    3.36      "no_notation"
    3.37      "no_syntax"
    3.38      "no_translations"
    3.39 +    "no_type_notation"
    3.40      "nonterminals"
    3.41      "notation"
    3.42      "oracle"
    3.43 @@ -404,6 +405,7 @@
    3.44      "text_raw"
    3.45      "theorems"
    3.46      "translations"
    3.47 +    "type_notation"
    3.48      "typed_print_translation"
    3.49      "typedecl"
    3.50      "types"
     4.1 --- a/etc/isar-keywords.el	Mon Mar 01 17:09:42 2010 +0100
     4.2 +++ b/etc/isar-keywords.el	Mon Mar 01 17:12:43 2010 +0100
     4.3 @@ -37,7 +37,6 @@
     4.4      "attribute_setup"
     4.5      "automaton"
     4.6      "ax_specification"
     4.7 -    "axclass"
     4.8      "axiomatization"
     4.9      "axioms"
    4.10      "back"
    4.11 @@ -145,6 +144,7 @@
    4.12      "no_notation"
    4.13      "no_syntax"
    4.14      "no_translations"
    4.15 +    "no_type_notation"
    4.16      "nominal_datatype"
    4.17      "nominal_inductive"
    4.18      "nominal_inductive2"
    4.19 @@ -252,6 +252,7 @@
    4.20      "txt"
    4.21      "txt_raw"
    4.22      "typ"
    4.23 +    "type_notation"
    4.24      "typed_print_translation"
    4.25      "typedecl"
    4.26      "typedef"
    4.27 @@ -451,7 +452,6 @@
    4.28      "atom_decl"
    4.29      "attribute_setup"
    4.30      "automaton"
    4.31 -    "axclass"
    4.32      "axiomatization"
    4.33      "axioms"
    4.34      "boogie_end"
    4.35 @@ -509,6 +509,7 @@
    4.36      "no_notation"
    4.37      "no_syntax"
    4.38      "no_translations"
    4.39 +    "no_type_notation"
    4.40      "nominal_datatype"
    4.41      "nonterminals"
    4.42      "notation"
    4.43 @@ -535,6 +536,7 @@
    4.44      "text_raw"
    4.45      "theorems"
    4.46      "translations"
    4.47 +    "type_notation"
    4.48      "typed_print_translation"
    4.49      "typedecl"
    4.50      "types"