src/Pure/Isar/isar_syn.ML
changeset 24950 106fc30769a9
parent 24938 a220317465b4
child 24953 f92386569176
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Oct 10 17:31:56 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Oct 10 17:31:58 2007 +0200
     1.3 @@ -243,10 +243,16 @@
     1.4          Toplevel.local_theory loc (Specification.abbreviation_cmd mode args)));
     1.5  
     1.6  val _ =
     1.7 -  OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
     1.8 +  OuterSyntax.command "notation" "add notation for constants / fixed variables" K.thy_decl
     1.9      (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
    1.10      >> (fn ((loc, mode), args) =>
    1.11 -        Toplevel.local_theory loc (Specification.notation_cmd mode args)));
    1.12 +        Toplevel.local_theory loc (Specification.notation_cmd true mode args)));
    1.13 +
    1.14 +val _ =
    1.15 +  OuterSyntax.command "no_notation" "delete notation for constants / fixed variables" K.thy_decl
    1.16 +    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
    1.17 +    >> (fn ((loc, mode), args) =>
    1.18 +        Toplevel.local_theory loc (Specification.notation_cmd false mode args)));
    1.19  
    1.20  
    1.21  (* constant specifications *)