# HG changeset patch
# User wenzelm
# Date 1192026551 -7200
# Node ID 16cb899de153af9d64a1ae93c7e8cfcf9578fc3c
# Parent  5f5679e2ec2f7be7d78add80a58a11406558d619
added no_notation;

diff -r 5f5679e2ec2f -r 16cb899de153 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Wed Oct 10 15:05:42 2007 +0200
+++ b/doc-src/IsarRef/generic.tex	Wed Oct 10 16:29:11 2007 +0200
@@ -7,7 +7,7 @@
 \indexisarcmd{axiomatization}
 \indexisarcmd{definition}\indexisaratt{defn}
 \indexisarcmd{abbreviation}\indexisarcmd{print-abbrevs}
-\indexisarcmd{notation}
+\indexisarcmd{notation}\indexisarcmd{no-notation}
 \begin{matharray}{rcll}
   \isarcmd{axiomatization} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
   \isarcmd{definition} & : & \isarkeep{local{\dsh}theory} \\
@@ -15,6 +15,7 @@
   \isarcmd{abbreviation} & : & \isarkeep{local{\dsh}theory} \\
   \isarcmd{print_abbrevs}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{notation} & : & \isarkeep{local{\dsh}theory} \\
+  \isarcmd{no_notation} & : & \isarkeep{local{\dsh}theory} \\
 \end{matharray}
 
 These specification mechanisms provide a slightly more abstract view
@@ -30,7 +31,7 @@
   ;
   'abbreviation' target? mode? (decl 'where')? prop
   ;
-  'notation' target? mode? (nameref mixfix + 'and')
+  ('notation' | 'no\_notation') target? mode? (nameref mixfix + 'and')
   ;
 
   fixes: ((name ('::' type)? mixfix? | vars) + 'and')
@@ -92,9 +93,13 @@
   (\S\ref{sec:syn-trans}).  Type declaration and internal syntactic
   representation of the given entity is retrieved from the context.
   
+\item $\isarkeyword{no_notation}$ is similar to
+$\isarkeyword{notation}$, but removes the specified syntax annotation
+from the present context.
+
 \end{descr}
 
-All of these specifications support local theory targets (cf.\ 
+All of these specifications support local theory targets (cf.\
 \S\ref{sec:target}).