src/Pure/Isar/isar_syn.ML

 
 (* classes and sorts *)
 
 val _ =
   Outer_Syntax.command @{command_spec "classes"} "declare type classes"
-    (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<") |--
+    (Scan.repeat1 (Parse.binding -- Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<"}) |--
         Parse.!!! (Parse.list1 Parse.class)) [])
       >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "classrel"} "state inclusion of type classes (axiomatic!)"
-    (Parse.and_list1 (Parse.class -- ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<")
+    (Parse.and_list1 (Parse.class -- ((@{keyword "\<subseteq>"} || @{keyword "<"})
         |-- Parse.!!! Parse.class))
     >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "default_sort"}

       >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "type_synonym"} "declare type abbreviation"
     (Parse.type_args -- Parse.binding --
-      (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
+      (@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
       >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
 
 val _ =
   Outer_Syntax.command @{command_spec "nonterminal"}
     "declare syntactic type constructors (grammar nonterminal symbols)"

 val _ =
   Outer_Syntax.command @{command_spec "consts"} "declare constants"
     (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
 
 val mode_spec =
-  (Parse.$$$ "output" >> K ("", false)) ||
-    Parse.name -- Scan.optional (Parse.$$$ "output" >> K false) true;
+  (@{keyword "output"} >> K ("", false)) ||
+    Parse.name -- Scan.optional (@{keyword "output"} >> K false) true;
 
 val opt_mode =
-  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (mode_spec --| Parse.$$$ ")")) Syntax.mode_default;
+  Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default;
 
 val _ =
   Outer_Syntax.command @{command_spec "syntax"} "declare syntactic constants"
     (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
 

 
 (* translations *)
 
 val trans_pat =
   Scan.optional
-    (Parse.$$$ "(" |-- Parse.!!! (Parse.xname --| Parse.$$$ ")")) "logic"
+    (@{keyword "("} |-- Parse.!!! (Parse.xname --| @{keyword ")"})) "logic"
     -- Parse.inner_syntax Parse.string;
 
 fun trans_arrow toks =
-  ((Parse.$$$ "\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.Parse_Rule ||
-    (Parse.$$$ "\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.Print_Rule ||
-    (Parse.$$$ "\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.Parse_Print_Rule) toks;
+  ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"}) >> K Syntax.Parse_Rule ||
+    (@{keyword "\<leftharpoondown>"} || @{keyword "<="}) >> K Syntax.Print_Rule ||
+    (@{keyword "\<rightleftharpoons>"} || @{keyword "=="}) >> K Syntax.Parse_Print_Rule) toks;
 
 val trans_line =
   trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
     >> (fn (left, (arr, right)) => arr (left, right));
 

       (fn spec => Toplevel.theory (fn thy =>
         (legacy_feature "Old 'axioms' command -- use 'axiomatization' instead";
           Isar_Cmd.add_axioms spec thy))));
 
 val opt_unchecked_overloaded =
-  Scan.optional (Parse.$$$ "(" |-- Parse.!!!
-    (((Parse.$$$ "unchecked" >> K true) -- Scan.optional (Parse.$$$ "overloaded" >> K true) false ||
-      Parse.$$$ "overloaded" >> K (false, true)) --| Parse.$$$ ")")) (false, false);
+  Scan.optional (@{keyword "("} |-- Parse.!!!
+    (((@{keyword "unchecked"} >> K true) --
+        Scan.optional (@{keyword "overloaded"} >> K true) false ||
+      @{keyword "overloaded"} >> K (false, true)) --| @{keyword ")"})) (false, false);
 
 val _ =
   Outer_Syntax.command @{command_spec "defs"} "define constants"
     (opt_unchecked_overloaded --
       Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))

     (Parse.ML_source >> Isar_Cmd.local_setup);
 
 val _ =
   Outer_Syntax.command @{command_spec "attribute_setup"} "define attribute in ML"
     (Parse.position Parse.name --
-        Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")
+        Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
       >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
 
 val _ =
   Outer_Syntax.command @{command_spec "method_setup"} "define proof method in ML"
     (Parse.position Parse.name --
-        Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")
+        Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
       >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "declaration"} "generic ML declaration"
     (Parse.opt_keyword "pervasive" -- Parse.ML_source

       >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "simproc_setup"} "define simproc in ML"
     (Parse.position Parse.name --
-      (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
-      Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
+      (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) --
+      Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
     >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
 
 
 (* translation functions *)
 

 
 (* oracles *)
 
 val _ =
   Outer_Syntax.command @{command_spec "oracle"} "declare oracle"
-    (Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>
+    (Parse.position Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
       (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
 
 
 (* bundled declarations *)
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "bundle"} "define bundle of declarations"
-    ((Parse.binding --| Parse.$$$ "=") -- Parse_Spec.xthms1 -- Parse.for_fixes
+    ((Parse.binding --| @{keyword "="}) -- Parse_Spec.xthms1 -- Parse.for_fixes
       >> (uncurry Bundle.bundle_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "include"}
     "include declarations from bundle in proof body"

 
 (* locales *)
 
 val locale_val =
   Parse_Spec.locale_expression false --
-    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
+    Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
 
 val _ =
   Outer_Syntax.command @{command_spec "locale"} "define named proof context"
     (Parse.binding --
-      Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
+      Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
             (Expression.add_locale_cmd I name Binding.empty expr elems #> snd)));
 
 fun parse_interpretation_arguments mandatory =

       (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
 
 val _ =
   Outer_Syntax.command @{command_spec "sublocale"}
     "prove sublocale relation between a locale and a locale expression"
-    (Parse.position Parse.xname --| (Parse.$$$ "\<subseteq>" || Parse.$$$ "<") --
+    (Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
       parse_interpretation_arguments false
       >> (fn (loc, (expr, equations)) =>
           Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
 
 val _ =

 
 (* classes *)
 
 val class_val =
   Parse_Spec.class_expression --
-    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
+    Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   Scan.repeat1 Parse_Spec.context_element >> pair [];
 
 val _ =
   Outer_Syntax.command @{command_spec "class"} "define type class"
-   (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin
+   (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
         (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
           (Class_Declaration.class_cmd I name supclasses elems #> snd)));
 
 val _ =

          Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
 
 val _ =
   Outer_Syntax.command @{command_spec "instance"} "prove type arity or subclass relation"
   ((Parse.class --
-    ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
+    ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
     Parse.multi_arity >> Class.instance_arity_cmd)
     >> (Toplevel.print oo Toplevel.theory_to_proof) ||
     Scan.succeed
       (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
 
 
 (* arbitrary overloading *)
 
 val _ =
   Outer_Syntax.command @{command_spec "overloading"} "overloaded definitions"
-   (Scan.repeat1 (Parse.name --| (Parse.$$$ "\<equiv>" || Parse.$$$ "==") -- Parse.term --
-      Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
+   (Scan.repeat1 (Parse.name --| (@{keyword "\<equiv>"} || @{keyword "=="}) -- Parse.term --
+      Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
       >> Parse.triple1) --| Parse.begin
    >> (fn operations => Toplevel.print o
          Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
 
 

 val _ =
   Outer_Syntax.command @{command_spec "def"} "local definition"
     (Parse.and_list1
       (Parse_Spec.opt_thm_name ":" --
         ((Parse.binding -- Parse.opt_mixfix) --
-          ((Parse.$$$ "\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp)))
+          ((@{keyword "\<equiv>"} || @{keyword "=="}) |-- Parse.!!! Parse.termp)))
     >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
 
 val _ =
   Outer_Syntax.command @{command_spec "obtain"} "generalized elimination"
     (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement

   Outer_Syntax.command @{command_spec "guess"} "wild guessing (unstructured)"
     (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
 
 val _ =
   Outer_Syntax.command @{command_spec "let"} "bind text variables"
-    (Parse.and_list1 (Parse.and_list1 Parse.term -- (Parse.$$$ "=" |-- Parse.term))
+    (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
       >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
 
 val _ =
   Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables"
     (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
     >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
 
 val case_spec =
-  (Parse.$$$ "(" |--
-    Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.binding) --| Parse.$$$ ")") ||
+  (@{keyword "("} |--
+    Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.binding) --| @{keyword ")"}) ||
     Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
 
 val _ =
   Outer_Syntax.command @{command_spec "case"} "invoke local context"
     (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));

 
 
 (* calculational proof commands *)
 
 val calc_args =
-  Scan.option (Parse.$$$ "(" |-- Parse.!!! ((Parse_Spec.xthms1 --| Parse.$$$ ")")));
+  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"})));
 
 val _ =
   Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
     (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
 

 
 
 (** diagnostic commands (for interactive mode only) **)
 
 val opt_modes =
-  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
-
-val opt_bang = Scan.optional (Parse.$$$ "!" >> K true) false;
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+
+val opt_bang = Scan.optional (@{keyword "!"} >> K true) false;
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "pretty_setmargin"}
     "change default margin for pretty printing"
     (Parse.nat >>