allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;

--- a/NEWS	Thu Apr 29 17:29:53 2010 +0200
+++ b/NEWS	Thu Apr 29 17:47:53 2010 +0200
@@ -64,6 +64,11 @@
 
 * Type constructors admit general mixfix syntax, not just infix.
 
+* Concrete syntax may be attached to local entities without a proof
+body, too.  This works via regular mixfix annotations for 'fix',
+'def', 'obtain' etc. or via the explicit 'write' command, which is
+similar to the 'notation' command in theory specifications.
+
 * Use of cumulative prems via "!" in some proof methods has been
 discontinued (legacy feature).
 
@@ -7004,3 +7009,5 @@
 types;
 
 :mode=text:wrap=hard:maxLineLen=72:
+
+ LocalWords:  def

--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Apr 29 17:29:53 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Apr 29 17:47:53 2010 +0200
@@ -365,6 +365,7 @@
     @{command_def "no_type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def "write"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
   \end{matharray}
 
   \begin{rail}
@@ -372,6 +373,8 @@
     ;
     ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
     ;
+    'write' mode? (nameref structmixfix + 'and')
+    ;
   \end{rail}
 
   \begin{description}
@@ -392,12 +395,14 @@
   but removes the specified syntax annotation from the present
   context.
 
+  \item @{command "write"} is similar to @{command "notation"}, but
+  works within an Isar proof body.
+
   \end{description}
 
-  Compared to the underlying @{command "syntax"} and @{command
-  "no_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.
+  Note that the more primitive commands @{command "syntax"} and
+  @{command "no_syntax"} (\secref{sec:syn-trans}) provide raw access
+  to the syntax tables of a global theory.
 *}
 
 

--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Apr 29 17:29:53 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Apr 29 17:47:53 2010 +0200
@@ -388,6 +388,7 @@
     \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}} \\
+    \indexdef{}{command}{write}\hypertarget{command.write}{\hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
   \end{matharray}
 
   \begin{rail}
@@ -395,6 +396,8 @@
     ;
     ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
     ;
+    'write' mode? (nameref structmixfix + 'and')
+    ;
   \end{rail}
 
   \begin{description}
@@ -414,11 +417,14 @@
   but removes the specified syntax annotation from the present
   context.
 
+  \item \hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but
+  works within an Isar proof body.
+
   \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.%
+  Note that the more primitive commands \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and
+  \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}} (\secref{sec:syn-trans}) provide raw access
+  to the syntax tables of a global theory.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %