doc-src/IsarRef/generic.tex

 \subsection{Derived specifications}
 
 \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} \\
   defn & : & \isaratt \\
   \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
 than the underlying primitives of $\CONSTS$, $\DEFS$ (see
 \S\ref{sec:consts}), and $\isarkeyword{axioms}$ (see

   ;
   'definition' target? (decl 'where')? thmdecl? prop
   ;
   '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')
   ;
   specs: (thmdecl? props + 'and')

   existing constant or fixed variable.  This is a robust interface to
   the underlying $\isarkeyword{syntax}$ primitive
   (\S\ref{sec:syn-trans}).  Type declaration and internal syntactic
   representation of the given entity is retrieved from the context.
   
-\end{descr}
-
-All of these specifications support local theory targets (cf.\ 
+\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.\
 \S\ref{sec:target}).
 
 
 \subsection{Generic declarations}