doc-src/IsarRef/Thy/Inner_Syntax.thy
changeset 46288 8a2c5dc0b00e
parent 46287 0bb3d8ee5d25
child 46289 d0199d9f9c5b
--- 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')