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"