# HG changeset patch # User wenzelm # Date 1267459963 -3600 # Node ID cc8e4276d093e99a513de1087e4844cfcf0ae0be # Parent 4c7cba1f7ce937e71ecb1f32ddd0a829dbe48fde updated generated files; diff -r 4c7cba1f7ce9 -r cc8e4276d093 doc-src/IsarImplementation/Thy/document/Prelim.tex --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon Mar 01 17:09:42 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon Mar 01 17:12:43 2010 +0100 @@ -544,14 +544,14 @@ \ \ \ \ val\ empty\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline \ \ \ \ val\ extend\ {\isacharequal}\ I{\isacharsemicolon}\isanewline \ \ \ \ fun\ merge\ {\isacharparenleft}ts{\isadigit{1}}{\isacharcomma}\ ts{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ \ \ OrdList{\isachardot}union\ TermOrd{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ OrdList{\isachardot}union\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isacharsemicolon}\isanewline \ \ {\isacharparenright}\isanewline \isanewline \ \ val\ get\ {\isacharequal}\ Terms{\isachardot}get{\isacharsemicolon}\isanewline \isanewline \ \ fun\ add\ raw{\isacharunderscore}t\ thy\ {\isacharequal}\isanewline \ \ \ \ let\ val\ t\ {\isacharequal}\ Sign{\isachardot}cert{\isacharunderscore}term\ thy\ raw{\isacharunderscore}t\isanewline -\ \ \ \ in\ Terms{\isachardot}map\ {\isacharparenleft}OrdList{\isachardot}insert\ TermOrd{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ t{\isacharparenright}\ thy\ end{\isacharsemicolon}\isanewline +\ \ \ \ in\ Terms{\isachardot}map\ {\isacharparenleft}OrdList{\isachardot}insert\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ t{\isacharparenright}\ thy\ end{\isacharsemicolon}\isanewline \isanewline \ \ end{\isacharsemicolon}\isanewline {\isacharverbatimclose}% diff -r 4c7cba1f7ce9 -r cc8e4276d093 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Mar 01 17:09:42 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Mar 01 17:12:43 2010 +0100 @@ -378,34 +378,47 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsection{Explicit term notation% +\isamarkupsection{Explicit notation% } \isamarkuptrue% % \begin{isamarkuptext}% \begin{matharray}{rcll} + \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}} \\ + \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}} \\ \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ \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}} \\ \end{matharray} \begin{rail} + ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and') + ; ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and') ; \end{rail} \begin{description} + \item \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix + syntax with an existing type constructor. The arity of the + constructor is retrieved from the context. + + \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 + the present context. + \item \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix - syntax with an existing constant or fixed variable. This is a - robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive - (\secref{sec:syn-trans}). Type declaration and internal syntactic - representation of the given entity is retrieved from the context. + syntax with an existing constant or fixed variable. The type + declaration of the given entity is retrieved from the context. \item \hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but removes the specified syntax annotation from the present context. - \end{description}% + \end{description} + + 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 + provide explicit checking wrt.\ the logical context, and work within + general local theory targets, not just the global theory.% \end{isamarkuptext}% \isamarkuptrue% % diff -r 4c7cba1f7ce9 -r cc8e4276d093 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Mon Mar 01 17:09:42 2010 +0100 +++ b/etc/isar-keywords-ZF.el Mon Mar 01 17:12:43 2010 +0100 @@ -30,7 +30,6 @@ "arities" "assume" "attribute_setup" - "axclass" "axiomatization" "axioms" "back" @@ -108,6 +107,7 @@ "no_notation" "no_syntax" "no_translations" + "no_type_notation" "nonterminals" "notation" "note" @@ -189,6 +189,7 @@ "txt" "txt_raw" "typ" + "type_notation" "typed_print_translation" "typedecl" "types" @@ -348,7 +349,6 @@ "abbreviation" "arities" "attribute_setup" - "axclass" "axiomatization" "axioms" "class" @@ -385,6 +385,7 @@ "no_notation" "no_syntax" "no_translations" + "no_type_notation" "nonterminals" "notation" "oracle" @@ -404,6 +405,7 @@ "text_raw" "theorems" "translations" + "type_notation" "typed_print_translation" "typedecl" "types" diff -r 4c7cba1f7ce9 -r cc8e4276d093 etc/isar-keywords.el --- a/etc/isar-keywords.el Mon Mar 01 17:09:42 2010 +0100 +++ b/etc/isar-keywords.el Mon Mar 01 17:12:43 2010 +0100 @@ -37,7 +37,6 @@ "attribute_setup" "automaton" "ax_specification" - "axclass" "axiomatization" "axioms" "back" @@ -145,6 +144,7 @@ "no_notation" "no_syntax" "no_translations" + "no_type_notation" "nominal_datatype" "nominal_inductive" "nominal_inductive2" @@ -252,6 +252,7 @@ "txt" "txt_raw" "typ" + "type_notation" "typed_print_translation" "typedecl" "typedef" @@ -451,7 +452,6 @@ "atom_decl" "attribute_setup" "automaton" - "axclass" "axiomatization" "axioms" "boogie_end" @@ -509,6 +509,7 @@ "no_notation" "no_syntax" "no_translations" + "no_type_notation" "nominal_datatype" "nonterminals" "notation" @@ -535,6 +536,7 @@ "text_raw" "theorems" "translations" + "type_notation" "typed_print_translation" "typedecl" "types"