# 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"