--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat Feb 04 15:44:50 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat Feb 04 15:56:49 2012 +0100
@@ -457,6 +457,13 @@
@{command_def "write"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
\end{matharray}
+ Commands that introduce new logical entities (terms or types)
+ usually allow to provide mixfix annotations on the spot, which is
+ convenient for default notation. Nonetheless, the syntax may be
+ modified later on by declarations for explicit notation. This
+ allows to add or delete mixfix annotations for of existing logical
+ entities within the current context.
+
@{rail "
(@@{command type_notation} | @@{command no_type_notation}) @{syntax target}?
@{syntax mode}? \\ (@{syntax nameref} @{syntax mixfix} + @'and')
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 04 15:44:50 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 04 15:56:49 2012 +0100
@@ -578,6 +578,13 @@
\indexdef{}{command}{write}\hypertarget{command.write}{\hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
\end{matharray}
+ Commands that introduce new logical entities (terms or types)
+ usually allow to provide mixfix annotations on the spot, which is
+ convenient for default notation. Nonetheless, the syntax may be
+ modified later on by declarations for explicit notation. This
+ allows to add or delete mixfix annotations for of existing logical
+ entities within the current context.
+
\begin{railoutput}
\rail@begin{5}{}
\rail@bar