src/Pure/Pure.thy

   Outer_Syntax.local_theory @{command_keyword local_setup} "ML setup for local theory"
     (Parse.ML_source >> Isar_Cmd.local_setup);
 
 val _ =
   Outer_Syntax.command @{command_keyword oracle} "declare oracle"
-    (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
+    (Parse.range Parse.name -- (@{keyword =} |-- Parse.ML_source) >>
       (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML"
     (Parse.position Parse.name --
-        Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
+        Parse.!!! (@{keyword =} |-- Parse.ML_source -- Scan.optional Parse.text "")
       >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword method_setup} "define proof method in ML"
     (Parse.position Parse.name --
-        Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
+        Parse.!!! (@{keyword =} |-- Parse.ML_source -- Scan.optional Parse.text "")
       >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword 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_keyword simproc_setup} "define simproc in ML"
     (Parse.position Parse.name --
-      (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) --
+      (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword =}) --
       Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c));
 
 in end\<close>
 
 

           Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd));
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
     (Parse.type_args -- Parse.binding --
-      (@{keyword "="} |-- 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));
 
 in end\<close>
 
 

   Scan.optional
     (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.name --| @{keyword ")"})) "logic"
     -- Parse.inner_syntax Parse.string;
 
 fun trans_arrow toks =
-  ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"}) >> K Syntax.Parse_Rule ||
-    (@{keyword "\<leftharpoondown>"} || @{keyword "<="}) >> K Syntax.Print_Rule ||
-    (@{keyword "\<rightleftharpoons>"} || @{keyword "=="}) >> 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));
 

 local
 
 val _ =
   Outer_Syntax.maybe_begin_local_theory @{command_keyword bundle}
     "define bundle of declarations"
-    ((Parse.binding --| @{keyword "="}) -- Parse.thms1 -- Parse.for_fixes
+    ((Parse.binding --| @{keyword =}) -- Parse.thms1 -- Parse.for_fixes
       >> (uncurry Bundle.bundle_cmd))
     (Parse.binding --| Parse.begin >> Bundle.init);
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword unbundle}

 ML \<open>
 local
 
 val locale_val =
   Parse_Spec.locale_expression --
-    Scan.optional (@{keyword "+"} |-- 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_keyword locale} "define named specification context"
     (Parse.binding --
-      Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
+      Scan.optional (@{keyword =} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           Toplevel.begin_local_theory begin
             (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
 
 val _ =

           Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
 
 val interpretation_args =
   Parse.!!! Parse_Spec.locale_expression --
     Scan.optional
-      (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
+      (@{keyword rewrites} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
 
 val _ =
   Outer_Syntax.command @{command_keyword interpret}
     "prove interpretation of locale expression in proof context"
     (interpretation_args >> (fn (expr, equations) =>
       Toplevel.proof (Interpretation.interpret_cmd expr equations)));
 
 val interpretation_args_with_defs =
   Parse.!!! Parse_Spec.locale_expression --
-    (Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
-      -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
+    (Scan.optional (@{keyword defines} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+      -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword =} -- Parse.term))) [] --
     Scan.optional
-      (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
+      (@{keyword rewrites} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation}
     "prove interpretation of locale expression into global theory"
     (interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
       Interpretation.global_interpretation_cmd expr defs equations));
 
 val _ =
   Outer_Syntax.command @{command_keyword sublocale}
     "prove sublocale relation between a locale and a locale expression"
-    ((Parse.position Parse.name --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
+    ((Parse.position Parse.name --| (@{keyword \<subseteq>} || @{keyword <}) --
       interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) =>
         Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations)))
     || interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
         Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs equations)));
 

 ML \<open>
 local
 
 val class_val =
   Parse_Spec.class_expression --
-    Scan.optional (@{keyword "+"} |-- 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_keyword class} "define type class"
-   (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
+   (Parse.binding -- Scan.optional (@{keyword =} |-- class_val) ([], []) -- Parse.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
         Toplevel.begin_local_theory begin
           (Class_Declaration.class_cmd name supclasses elems #> snd)));
 
 val _ =

      >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
 
 val _ =
   Outer_Syntax.command @{command_keyword instance} "prove type arity or subclass relation"
   ((Parse.class --
-    ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
+    ((@{keyword \<subseteq>} || @{keyword <}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
     Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
     Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I)));
 
 in end\<close>
 

 ML \<open>
 local
 
 val _ =
   Outer_Syntax.command @{command_keyword overloading} "overloaded definitions"
-   (Scan.repeat1 (Parse.name --| (@{keyword "=="} || @{keyword "\<equiv>"}) -- Parse.term --
-      Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
+   (Scan.repeat1 (Parse.name --| (@{keyword ==} || @{keyword \<equiv>}) -- Parse.term --
+      Scan.optional (@{keyword "("} |-- (@{keyword unchecked} >> K false) --| @{keyword ")"}) true
       >> Scan.triple1) --| Parse.begin
    >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
 
 in end\<close>
 

 val _ =
   Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
     (Parse.and_list1
       (Parse_Spec.opt_thm_name ":" --
         ((Parse.binding -- Parse.opt_mixfix) --
-          ((@{keyword "\<equiv>"} || @{keyword "=="}) |-- Parse.!!! Parse.termp)))
+          ((@{keyword \<equiv>} || @{keyword ==}) |-- Parse.!!! Parse.termp)))
     >> (fn args => Toplevel.proof (fn state =>
         (legacy_feature "Old 'def' command -- use 'define' instead"; Proof.def_cmd args state))));
 
 val _ =
   Outer_Syntax.command @{command_keyword consider} "state cases rule"

   Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
     (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd));
 
 val _ =
   Outer_Syntax.command @{command_keyword let} "bind text variables"
-    (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
+    (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword =} |-- Parse.term))
       >> (Toplevel.proof o Proof.let_bind_cmd));
 
 val _ =
   Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)

   Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
     Binding.empty_atts;
 
 val for_params =
   Scan.optional
-    (@{keyword "for"} |--
+    (@{keyword for} |--
       Parse.!!! ((Scan.option Parse.dots >> is_some) --
         (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
     (false, []);
 
 val _ =
   Outer_Syntax.command @{command_keyword subgoal}
     "focus on first subgoal within backward refinement"
-    (opt_fact_binding -- (Scan.option (@{keyword "premises"} |-- Parse.!!! opt_fact_binding)) --
+    (opt_fact_binding -- (Scan.option (@{keyword premises} |-- Parse.!!! opt_fact_binding)) --
       for_params >> (fn ((a, b), c) =>
         Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
 
 in end\<close>
 

   Outer_Syntax.command @{command_keyword term} "read and print term"
     (opt_modes -- Parse.term >> Isar_Cmd.print_term);
 
 val _ =
   Outer_Syntax.command @{command_keyword typ} "read and print type"
-    (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
+    (opt_modes -- (Parse.typ -- Scan.option (@{keyword ::} |-- Parse.!!! Parse.sort))
       >> Isar_Cmd.print_type);
 
 val _ =
   Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
     (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));