# HG changeset patch
# User wenzelm
# Date 1192030318 -7200
# Node ID 106fc30769a92705bd9f48156c3ea52f21e0445e
# Parent  5f00e3532418cc216dcad1be061c51c247234fed
added 'no_notation';

diff -r 5f00e3532418 -r 106fc30769a9 NEWS
--- a/NEWS	Wed Oct 10 17:31:56 2007 +0200
+++ b/NEWS	Wed Oct 10 17:31:58 2007 +0200
@@ -371,8 +371,10 @@
 
 * Isar/locales: 'notation' provides a robust interface to the 'syntax'
 primitive that also works in a locale context (both for constants and
-fixed variables).  Type declaration and internal syntactic
-representation of given constants retrieved from the context.
+fixed variables). Type declaration and internal syntactic representation
+of given constants retrieved from the context. Likewise, the
+'no_notation' command allows to remove given syntax annotations from the
+current context.
 
 * Isar/locales: new derived specification elements 'axiomatization',
 'definition', 'abbreviation', which support type-inference, admit
diff -r 5f00e3532418 -r 106fc30769a9 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Oct 10 17:31:56 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Oct 10 17:31:58 2007 +0200
@@ -243,10 +243,16 @@
         Toplevel.local_theory loc (Specification.abbreviation_cmd mode args)));
 
 val _ =
-  OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
+  OuterSyntax.command "notation" "add notation for constants / fixed variables" K.thy_decl
     (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
     >> (fn ((loc, mode), args) =>
-        Toplevel.local_theory loc (Specification.notation_cmd mode args)));
+        Toplevel.local_theory loc (Specification.notation_cmd true mode args)));
+
+val _ =
+  OuterSyntax.command "no_notation" "delete notation for constants / fixed variables" K.thy_decl
+    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
+    >> (fn ((loc, mode), args) =>
+        Toplevel.local_theory loc (Specification.notation_cmd false mode args)));
 
 
 (* constant specifications *)