# HG changeset patch # User wenzelm # Date 1512583173 -3600 # Node ID dea94b1aabc3c1480acc3328cff6660c20820b84 # Parent 909dcdec21221f6dd9dbb5c86729c734ba905768 prefer control symbol antiquotations; diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/Isar/attrib.ML Wed Dec 06 18:59:33 2017 +0100 @@ -489,38 +489,38 @@ (* theory setup *) val _ = Theory.setup - (setup @{binding tagged} (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #> - setup @{binding untagged} (Scan.lift Args.name >> Thm.untag) "untagged theorem" #> - setup @{binding kind} (Scan.lift Args.name >> Thm.kind) "theorem kind" #> - setup @{binding THEN} + (setup \<^binding>\tagged\ (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #> + setup \<^binding>\untagged\ (Scan.lift Args.name >> Thm.untag) "untagged theorem" #> + setup \<^binding>\kind\ (Scan.lift Args.name >> Thm.kind) "theorem kind" #> + setup \<^binding>\THEN\ (Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))) "resolution with rule" #> - setup @{binding OF} + setup \<^binding>\OF\ (thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))) "rule resolved with facts" #> - setup @{binding rename_abs} + setup \<^binding>\rename_abs\ (Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs => Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))) "rename bound variables in abstractions" #> - setup @{binding unfolded} + setup \<^binding>\unfolded\ (thms >> (fn ths => Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))) "unfolded definitions" #> - setup @{binding folded} + setup \<^binding>\folded\ (thms >> (fn ths => Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))) "folded definitions" #> - setup @{binding consumes} + setup \<^binding>\consumes\ (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes) "number of consumed facts" #> - setup @{binding constraints} + setup \<^binding>\constraints\ (Scan.lift Parse.nat >> Rule_Cases.constraints) "number of equality constraints" #> - setup @{binding cases_open} + setup \<^binding>\cases_open\ (Scan.succeed Rule_Cases.cases_open) "rule with open parameters" #> - setup @{binding case_names} + setup \<^binding>\case_names\ (Scan.lift (Scan.repeat (Args.name -- Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") [])) >> (fn cs => @@ -528,37 +528,37 @@ (map #1 cs) (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))) "named rule cases" #> - setup @{binding case_conclusion} + setup \<^binding>\case_conclusion\ (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion) "named conclusion of rule cases" #> - setup @{binding params} + setup \<^binding>\params\ (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params) "named rule parameters" #> - setup @{binding rule_format} + setup \<^binding>\rule_format\ (Scan.lift (Args.mode "no_asm") >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)) "result put into canonical rule format" #> - setup @{binding elim_format} + setup \<^binding>\elim_format\ (Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))) "destruct rule turned into elimination rule format" #> - setup @{binding no_vars} + setup \<^binding>\no_vars\ (Scan.succeed (Thm.rule_attribute [] (fn context => fn th => let val ctxt = Variable.set_body false (Context.proof_of context); val ((_, [th']), _) = Variable.import true [th] ctxt; in th' end))) "imported schematic variables" #> - setup @{binding atomize} + setup \<^binding>\atomize\ (Scan.succeed Object_Logic.declare_atomize) "declaration of atomize rule" #> - setup @{binding rulify} + setup \<^binding>\rulify\ (Scan.succeed Object_Logic.declare_rulify) "declaration of rulify rule" #> - setup @{binding rotated} + setup \<^binding>\rotated\ (Scan.lift (Scan.optional Parse.int 1 >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))) "rotated theorem premises" #> - setup @{binding defn} + setup \<^binding>\defn\ (add_del Local_Defs.defn_add Local_Defs.defn_del) "declaration of definitional transformations" #> - setup @{binding abs_def} + setup \<^binding>\abs_def\ (Scan.succeed (Thm.rule_attribute [] (Local_Defs.abs_def_rule o Context.proof_of))) "abstract over free variables of definitional theorem" #> diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/Isar/calculation.ML Wed Dec 06 18:59:33 2017 +0100 @@ -126,11 +126,11 @@ (* concrete syntax *) val _ = Theory.setup - (Attrib.setup @{binding trans} (Attrib.add_del trans_add trans_del) + (Attrib.setup \<^binding>\trans\ (Attrib.add_del trans_add trans_del) "declaration of transitivity rule" #> - Attrib.setup @{binding sym} (Attrib.add_del sym_add sym_del) + Attrib.setup \<^binding>\sym\ (Attrib.add_del sym_add sym_del) "declaration of symmetry rule" #> - Attrib.setup @{binding symmetric} (Scan.succeed symmetric) + Attrib.setup \<^binding>\symmetric\ (Scan.succeed symmetric) "resolution with symmetry rule" #> Global_Theory.add_thms [((Binding.empty, transitive_thm), [trans_add]), diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/Isar/class.ML Wed Dec 06 18:59:33 2017 +0100 @@ -782,9 +782,9 @@ standard_intro_classes_tac ctxt facts; val _ = Theory.setup - (Method.setup @{binding intro_classes} (Scan.succeed (METHOD o intro_classes_tac)) + (Method.setup \<^binding>\intro_classes\ (Scan.succeed (METHOD o intro_classes_tac)) "back-chain introduction rules of classes" #> - Method.setup @{binding standard} (Scan.succeed (METHOD o standard_tac)) + Method.setup \<^binding>\standard\ (Scan.succeed (METHOD o standard_tac)) "standard proof step: Pure intro/elim rule or class introduction"); diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/Isar/code.ML Wed Dec 06 18:59:33 2017 +0100 @@ -1264,7 +1264,7 @@ structure Codetype_Plugin = Plugin(type T = string); -val codetype_plugin = Plugin_Name.declare_setup @{binding codetype}; +val codetype_plugin = Plugin_Name.declare_setup \<^binding>\codetype\; fun type_interpretation f = Codetype_Plugin.interpretation codetype_plugin @@ -1539,7 +1539,7 @@ || Scan.succeed (code_attribute add_maybe_abs_eqn_liberal); in - Attrib.setup @{binding code} (Scan.lift code_attribute_parser) + Attrib.setup \<^binding>\code\ (Scan.lift code_attribute_parser) "declare theorems for code generation" end); diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/Isar/context_rules.ML Wed Dec 06 18:59:33 2017 +0100 @@ -219,13 +219,13 @@ Scan.option Parse.nat) >> (fn (f, n) => f n)) x; val _ = Theory.setup - (Attrib.setup @{binding intro} (add intro_bang intro intro_query) + (Attrib.setup \<^binding>\intro\ (add intro_bang intro intro_query) "declaration of introduction rule" #> - Attrib.setup @{binding elim} (add elim_bang elim elim_query) + Attrib.setup \<^binding>\elim\ (add elim_bang elim elim_query) "declaration of elimination rule" #> - Attrib.setup @{binding dest} (add dest_bang dest dest_query) + Attrib.setup \<^binding>\dest\ (add dest_bang dest dest_query) "declaration of destruction rule" #> - Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del) + Attrib.setup \<^binding>\rule\ (Scan.lift Args.del >> K rule_del) "remove declaration of intro/elim/dest rule"); end; diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Wed Dec 06 18:59:33 2017 +0100 @@ -211,9 +211,9 @@ val diag_goal = Proof.goal o Toplevel.proof_of o diag_state; val _ = Theory.setup - (ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state}) + (ML_Antiquotation.value (Binding.qualify true "Isar" \<^binding>\state\) (Scan.succeed "Isar_Cmd.diag_state ML_context") #> - ML_Antiquotation.value (Binding.qualify true "Isar" @{binding goal}) + ML_Antiquotation.value (Binding.qualify true "Isar" \<^binding>\goal\) (Scan.succeed "Isar_Cmd.diag_goal ML_context")); diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/Isar/locale.ML Wed Dec 06 18:59:33 2017 +0100 @@ -678,9 +678,9 @@ val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac; val _ = Theory.setup - (Method.setup @{binding intro_locales} (Scan.succeed (METHOD o try_intro_locales_tac false)) + (Method.setup \<^binding>\intro_locales\ (Scan.succeed (METHOD o try_intro_locales_tac false)) "back-chain introduction rules of locales without unfolding predicates" #> - Method.setup @{binding unfold_locales} (Scan.succeed (METHOD o try_intro_locales_tac true)) + Method.setup \<^binding>\unfold_locales\ (Scan.succeed (METHOD o try_intro_locales_tac true)) "back-chain all introduction rules of locales"); diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/Isar/method.ML Wed Dec 06 18:59:33 2017 +0100 @@ -266,7 +266,7 @@ (* rule etc. -- single-step refinements *) -val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false); +val rule_trace = Attrib.setup_config_bool \<^binding>\rule_trace\ (fn _ => false); fun trace ctxt rules = if Config.get ctxt rule_trace andalso not (null rules) then @@ -795,13 +795,13 @@ (* theory setup *) val _ = Theory.setup - (setup @{binding fail} (Scan.succeed (K fail)) "force failure" #> - setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #> - setup @{binding sleep} (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s))) + (setup \<^binding>\fail\ (Scan.succeed (K fail)) "force failure" #> + setup \<^binding>\succeed\ (Scan.succeed (K succeed)) "succeed" #> + setup \<^binding>\sleep\ (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s))) "succeed after delay (in seconds)" #> - setup @{binding "-"} (Scan.succeed (K (SIMPLE_METHOD all_tac))) + setup \<^binding>\-\ (Scan.succeed (K (SIMPLE_METHOD all_tac))) "insert current facts, nothing else" #> - setup @{binding goal_cases} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn _ => + setup \<^binding>\goal_cases\ (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn _ => CONTEXT_METHOD (fn _ => fn (ctxt, st) => (case drop (Thm.nprems_of st) names of [] => NONE @@ -813,36 +813,36 @@ |> (fn SOME msg => Seq.single (Seq.Error msg) | NONE => goal_cases_tac (map Token.content_of names) (ctxt, st))))) "bind cases for goals" #> - setup @{binding insert} (Attrib.thms >> (K o insert)) + setup \<^binding>\insert\ (Attrib.thms >> (K o insert)) "insert theorems, ignoring facts" #> - setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths)) + setup \<^binding>\intro\ (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths)) "repeatedly apply introduction rules" #> - setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths)) + setup \<^binding>\elim\ (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths)) "repeatedly apply elimination rules" #> - setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #> - setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #> - setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize) + setup \<^binding>\unfold\ (Attrib.thms >> unfold_meth) "unfold definitions" #> + setup \<^binding>\fold\ (Attrib.thms >> fold_meth) "fold definitions" #> + setup \<^binding>\atomize\ (Scan.lift (Args.mode "full") >> atomize) "present local premises as object-level statements" #> - setup @{binding rule} (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths)) + setup \<^binding>\rule\ (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths)) "apply some intro/elim rule" #> - setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #> - setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #> - setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #> - setup @{binding this} (Scan.succeed this) "apply current facts as rules" #> - setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #> - setup @{binding assumption} (Scan.succeed assumption) + setup \<^binding>\erule\ (xrule_meth erule) "apply rule in elimination manner (improper)" #> + setup \<^binding>\drule\ (xrule_meth drule) "apply rule in destruct manner (improper)" #> + setup \<^binding>\frule\ (xrule_meth frule) "apply rule in forward manner (improper)" #> + setup \<^binding>\this\ (Scan.succeed this) "apply current facts as rules" #> + setup \<^binding>\fact\ (Attrib.thms >> fact) "composition by facts from context" #> + setup \<^binding>\assumption\ (Scan.succeed assumption) "proof by assumption, preferring facts" #> - setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >> + setup \<^binding>\rename_tac\ (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >> (fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs)))) "rename parameters of goal" #> - setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >> + setup \<^binding>\rotate_tac\ (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >> (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i)))) "rotate assumptions of goal" #> - setup @{binding tactic} (parse_tactic >> (K o METHOD)) + setup \<^binding>\tactic\ (parse_tactic >> (K o METHOD)) "ML tactic as proof method" #> - setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac)) + setup \<^binding>\raw_tactic\ (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac)) "ML tactic as raw proof method" #> - setup @{binding use} + setup \<^binding>\use\ (Attrib.thms -- (Scan.lift (Parse.$$$ "in") |-- text_closure) >> (fn (thms, text) => fn ctxt => fn _ => evaluate_runtime text ctxt thms)) "indicate method facts and context for method expression"); diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/Isar/overloading.ML Wed Dec 06 18:59:33 2017 +0100 @@ -92,7 +92,7 @@ | SOME t' => if t aconv t' then NONE else SOME t'); val show_reverted_improvements = - Attrib.setup_config_bool @{binding "show_reverted_improvements"} (K true); + Attrib.setup_config_bool \<^binding>\show_reverted_improvements\ (K true); fun improve_term_uncheck ts ctxt = let diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/ML/ml_antiquotations.ML Wed Dec 06 18:59:33 2017 +0100 @@ -10,13 +10,13 @@ (* ML support *) val _ = Theory.setup - (ML_Antiquotation.inline @{binding undefined} + (ML_Antiquotation.inline \<^binding>\undefined\ (Scan.succeed "(raise General.Match)") #> - ML_Antiquotation.inline @{binding assert} + ML_Antiquotation.inline \<^binding>\assert\ (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> - ML_Antiquotation.declaration @{binding print} + ML_Antiquotation.declaration \<^binding>\print\ (Scan.lift (Scan.optional Args.embedded "Output.writeln")) (fn src => fn output => fn ctxt => let @@ -31,7 +31,7 @@ "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))"; in (K (env, body), ctxt') end) #> - ML_Antiquotation.value @{binding rat} + ML_Antiquotation.value \<^binding>\rat\ (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat -- Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) => "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b)))) @@ -40,7 +40,7 @@ (* formal entities *) val _ = Theory.setup - (ML_Antiquotation.value @{binding system_option} + (ML_Antiquotation.value \<^binding>\system_option\ (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => let val markup = @@ -56,35 +56,35 @@ val _ = Context_Position.report ctxt pos markup; in ML_Syntax.print_string name end)) #> - ML_Antiquotation.value @{binding theory} + ML_Antiquotation.value \<^binding>\theory\ (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => (Theory.check ctxt (name, pos); "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name)) || Scan.succeed "Proof_Context.theory_of ML_context") #> - ML_Antiquotation.value @{binding theory_context} + ML_Antiquotation.value \<^binding>\theory_context\ (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => (Theory.check ctxt (name, pos); "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))) #> - ML_Antiquotation.inline @{binding context} + ML_Antiquotation.inline \<^binding>\context\ (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #> - ML_Antiquotation.inline @{binding typ} (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> - ML_Antiquotation.inline @{binding term} (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> - ML_Antiquotation.inline @{binding prop} (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> + ML_Antiquotation.inline \<^binding>\typ\ (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> + ML_Antiquotation.inline \<^binding>\term\ (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> + ML_Antiquotation.inline \<^binding>\prop\ (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> - ML_Antiquotation.value @{binding ctyp} (Args.typ >> (fn T => + ML_Antiquotation.value \<^binding>\ctyp\ (Args.typ >> (fn T => "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> - ML_Antiquotation.value @{binding cterm} (Args.term >> (fn t => + ML_Antiquotation.value \<^binding>\cterm\ (Args.term >> (fn t => "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> - ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t => + ML_Antiquotation.value \<^binding>\cprop\ (Args.prop >> (fn t => "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> - ML_Antiquotation.inline @{binding method} + ML_Antiquotation.inline \<^binding>\method\ (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => ML_Syntax.print_string (Method.check_name ctxt (name, pos))))); @@ -92,7 +92,7 @@ (* locales *) val _ = Theory.setup - (ML_Antiquotation.inline @{binding locale} + (ML_Antiquotation.inline \<^binding>\locale\ (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => Locale.check (Proof_Context.theory_of ctxt) (name, pos) |> ML_Syntax.print_string))); @@ -106,10 +106,10 @@ |> ML_Syntax.print_string); val _ = Theory.setup - (ML_Antiquotation.inline @{binding class} (class false) #> - ML_Antiquotation.inline @{binding class_syntax} (class true) #> + (ML_Antiquotation.inline \<^binding>\class\ (class false) #> + ML_Antiquotation.inline \<^binding>\class_syntax\ (class true) #> - ML_Antiquotation.inline @{binding sort} + ML_Antiquotation.inline \<^binding>\sort\ (Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))); @@ -128,13 +128,13 @@ in ML_Syntax.print_string res end); val _ = Theory.setup - (ML_Antiquotation.inline @{binding type_name} + (ML_Antiquotation.inline \<^binding>\type_name\ (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> - ML_Antiquotation.inline @{binding type_abbrev} + ML_Antiquotation.inline \<^binding>\type_abbrev\ (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> - ML_Antiquotation.inline @{binding nonterminal} + ML_Antiquotation.inline \<^binding>\nonterminal\ (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> - ML_Antiquotation.inline @{binding type_syntax} + ML_Antiquotation.inline \<^binding>\type_syntax\ (type_name "type" (fn (c, _) => Lexicon.mark_type c))); @@ -149,20 +149,20 @@ in ML_Syntax.print_string res end); val _ = Theory.setup - (ML_Antiquotation.inline @{binding const_name} + (ML_Antiquotation.inline \<^binding>\const_name\ (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #> - ML_Antiquotation.inline @{binding const_abbrev} + ML_Antiquotation.inline \<^binding>\const_abbrev\ (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> - ML_Antiquotation.inline @{binding const_syntax} + ML_Antiquotation.inline \<^binding>\const_syntax\ (const_name (fn (_, c) => Lexicon.mark_const c)) #> - ML_Antiquotation.inline @{binding syntax_const} + ML_Antiquotation.inline \<^binding>\syntax_const\ (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (c, pos)) => if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c) then ML_Syntax.print_string c else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #> - ML_Antiquotation.inline @{binding const} + ML_Antiquotation.inline \<^binding>\const\ (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] >> (fn ((ctxt, (raw_c, pos)), Ts) => @@ -201,7 +201,7 @@ in val _ = Theory.setup - (ML_Antiquotation.value @{binding map} + (ML_Antiquotation.value \<^binding>\map\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ @@ -209,7 +209,7 @@ \ | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\ \ | map _" ^ dummy n ^ " = raise ListPair.UnequalLengths\n" ^ " in map f end")) #> - ML_Antiquotation.value @{binding fold} + ML_Antiquotation.value \<^binding>\fold\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ @@ -217,7 +217,7 @@ \ | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\ \ | fold _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ " in fold f end")) #> - ML_Antiquotation.value @{binding fold_map} + ML_Antiquotation.value \<^binding>\fold_map\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ @@ -229,7 +229,7 @@ \ in (x :: xs, a'') end\n\ \ | fold_map _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ " in fold_map f end")) #> - ML_Antiquotation.value @{binding split_list} + ML_Antiquotation.value \<^binding>\split_list\ (Scan.lift parameter >> (fn n => "fn list =>\n\ \ let\n\ @@ -238,7 +238,7 @@ \ let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\ \ in " ^ cons_tuple n ^ "end\n\ \ in split_list list end")) #> - ML_Antiquotation.value @{binding apply} + ML_Antiquotation.value \<^binding>\apply\ (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >> (fn (n, opt_index) => let @@ -259,14 +259,14 @@ (* outer syntax *) val _ = Theory.setup - (ML_Antiquotation.value @{binding keyword} + (ML_Antiquotation.value \<^binding>\keyword\ (Args.context -- Scan.lift (Parse.position (Parse.embedded || Parse.keyword_with (K true))) >> (fn (ctxt, (name, pos)) => if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name); "Parse.$$$ " ^ ML_Syntax.print_string name) else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #> - ML_Antiquotation.value @{binding command_keyword} + ML_Antiquotation.value \<^binding>\command_keyword\ (Args.context -- Scan.lift (Parse.position Parse.embedded) >> (fn (ctxt, (name, pos)) => (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of SOME markup => diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/ML/ml_thms.ML Wed Dec 06 18:59:33 2017 +0100 @@ -40,7 +40,7 @@ (* attribute source *) val _ = Theory.setup - (ML_Antiquotation.declaration @{binding attributes} Attrib.attribs + (ML_Antiquotation.declaration \<^binding>\attributes\ Attrib.attribs (fn _ => fn srcs => fn ctxt => let val i = serial () in ctxt @@ -69,8 +69,8 @@ in (decl, ctxt'') end; val _ = Theory.setup - (ML_Antiquotation.declaration @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #> - ML_Antiquotation.declaration @{binding thms} Attrib.thms (K (thm_binding "thms" false))); + (ML_Antiquotation.declaration \<^binding>\thm\ (Attrib.thm >> single) (K (thm_binding "thm" true)) #> + ML_Antiquotation.declaration \<^binding>\thms\ Attrib.thms (K (thm_binding "thms" false))); (* ad-hoc goals *) @@ -80,7 +80,7 @@ val goal = Scan.unless (by || and_) Args.embedded_inner_syntax; val _ = Theory.setup - (ML_Antiquotation.declaration @{binding lemma} + (ML_Antiquotation.declaration \<^binding>\lemma\ (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) -- (Parse.position by -- Method.parse -- Scan.option Method.parse))) (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt => diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/ML_Bootstrap.thy --- a/src/Pure/ML_Bootstrap.thy Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/ML_Bootstrap.thy Wed Dec 06 18:59:33 2017 +0100 @@ -34,7 +34,7 @@ \ \ -ML \@{assert} (not (can ML \open RunCall\))\ +ML \\<^assert> (not (can ML \open RunCall\))\ subsection \Switch to bootstrap environment\ diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/PIDE/resources.ML Wed Dec 06 18:59:33 2017 +0100 @@ -229,19 +229,19 @@ in val _ = Theory.setup - (Thy_Output.antiquotation @{binding path} (Scan.lift (Parse.position Parse.path)) + (Thy_Output.antiquotation \<^binding>\path\ (Scan.lift (Parse.position Parse.path)) (document_antiq NONE o #context) #> - Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path)) + Thy_Output.antiquotation \<^binding>\file\ (Scan.lift (Parse.position Parse.path)) (document_antiq (SOME File.check_file) o #context) #> - Thy_Output.antiquotation @{binding dir} (Scan.lift (Parse.position Parse.path)) + Thy_Output.antiquotation \<^binding>\dir\ (Scan.lift (Parse.position Parse.path)) (document_antiq (SOME File.check_dir) o #context) #> - ML_Antiquotation.value @{binding path} + ML_Antiquotation.value \<^binding>\path\ (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq NONE)) #> - ML_Antiquotation.value @{binding file} + ML_Antiquotation.value \<^binding>\file\ (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq (SOME File.check_file))) #> - ML_Antiquotation.value @{binding dir} + ML_Antiquotation.value \<^binding>\dir\ (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq (SOME File.check_dir)))); diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/Proof/extraction.ML Wed Dec 06 18:59:33 2017 +0100 @@ -470,9 +470,9 @@ "(realizes (r) (!!x. PROP P (x))) == \ \ (!!x. PROP realizes (r (x)) (PROP P (x)))"] #> - Attrib.setup @{binding extraction_expand} (Scan.succeed (extraction_expand false)) + Attrib.setup \<^binding>\extraction_expand\ (Scan.succeed (extraction_expand false)) "specify theorems to be expanded during extraction" #> - Attrib.setup @{binding extraction_expand_def} (Scan.succeed (extraction_expand true)) + Attrib.setup \<^binding>\extraction_expand_def\ (Scan.succeed (extraction_expand true)) "specify definitions to be expanded during extraction"); diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/Pure.thy Wed Dec 06 18:59:33 2017 +0100 @@ -110,7 +110,7 @@ subsection \External file dependencies\ ML \ - Outer_Syntax.command @{command_keyword external_file} "formal dependency on external file" + Outer_Syntax.command \<^command_keyword>\external_file\ "formal dependency on external file" (Parse.position Parse.path >> (fn (s, pos) => Toplevel.keep (fn st => let val ctxt = Toplevel.context_of st; @@ -126,38 +126,38 @@ ML \ local -val semi = Scan.option @{keyword ";"}; +val semi = Scan.option \<^keyword>\;\; val _ = - Outer_Syntax.command @{command_keyword ML_file} "read and evaluate Isabelle/ML file" + Outer_Syntax.command \<^command_keyword>\ML_file\ "read and evaluate Isabelle/ML file" (Resources.parse_files "ML_file" --| semi >> ML_File.ML NONE); val _ = - Outer_Syntax.command @{command_keyword ML_file_debug} + Outer_Syntax.command \<^command_keyword>\ML_file_debug\ "read and evaluate Isabelle/ML file (with debugger information)" (Resources.parse_files "ML_file_debug" --| semi >> ML_File.ML (SOME true)); val _ = - Outer_Syntax.command @{command_keyword ML_file_no_debug} + Outer_Syntax.command \<^command_keyword>\ML_file_no_debug\ "read and evaluate Isabelle/ML file (no debugger information)" (Resources.parse_files "ML_file_no_debug" --| semi >> ML_File.ML (SOME false)); val _ = - Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file" + Outer_Syntax.command \<^command_keyword>\SML_file\ "read and evaluate Standard ML file" (Resources.parse_files "SML_file" --| semi >> ML_File.SML NONE); val _ = - Outer_Syntax.command @{command_keyword SML_file_debug} + Outer_Syntax.command \<^command_keyword>\SML_file_debug\ "read and evaluate Standard ML file (with debugger information)" (Resources.parse_files "SML_file_debug" --| semi >> ML_File.SML (SOME true)); val _ = - Outer_Syntax.command @{command_keyword SML_file_no_debug} + Outer_Syntax.command \<^command_keyword>\SML_file_no_debug\ "read and evaluate Standard ML file (no debugger information)" (Resources.parse_files "SML_file_no_debug" --| semi >> ML_File.SML (SOME false)); val _ = - Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment" + Outer_Syntax.command \<^command_keyword>\SML_export\ "evaluate SML within Isabelle/ML environment" (Parse.ML_source >> (fn source => let val flags: ML_Compiler.flags = @@ -169,7 +169,7 @@ end)); val _ = - Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment" + Outer_Syntax.command \<^command_keyword>\SML_import\ "evaluate Isabelle/ML within SML environment" (Parse.ML_source >> (fn source => let val flags: ML_Compiler.flags = @@ -182,7 +182,7 @@ end)); val _ = - Outer_Syntax.command @{command_keyword ML_prf} "ML text within proof" + Outer_Syntax.command \<^command_keyword>\ML_prf\ "ML text within proof" (Parse.ML_source >> (fn source => Toplevel.proof (Proof.map_context (Context.proof_map (ML_Context.exec (fn () => @@ -190,52 +190,52 @@ Proof.propagate_ml_env))); val _ = - Outer_Syntax.command @{command_keyword ML_val} "diagnostic ML text" + Outer_Syntax.command \<^command_keyword>\ML_val\ "diagnostic ML text" (Parse.ML_source >> Isar_Cmd.ml_diag true); val _ = - Outer_Syntax.command @{command_keyword ML_command} "diagnostic ML text (silent)" + Outer_Syntax.command \<^command_keyword>\ML_command\ "diagnostic ML text (silent)" (Parse.ML_source >> Isar_Cmd.ml_diag false); val _ = - Outer_Syntax.command @{command_keyword setup} "ML setup for global theory" + Outer_Syntax.command \<^command_keyword>\setup\ "ML setup for global theory" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup)); val _ = - Outer_Syntax.local_theory @{command_keyword local_setup} "ML setup for local theory" + 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) >> + Outer_Syntax.command \<^command_keyword>\oracle\ "declare oracle" + (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" + 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" + 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" + Outer_Syntax.local_theory \<^command_keyword>\declaration\ "generic ML declaration" (Parse.opt_keyword "pervasive" -- Parse.ML_source >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt)); val _ = - Outer_Syntax.local_theory @{command_keyword syntax_declaration} "generic ML syntax declaration" + Outer_Syntax.local_theory \<^command_keyword>\syntax_declaration\ "generic ML syntax 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" + 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\ @@ -249,20 +249,20 @@ local val _ = - Outer_Syntax.local_theory @{command_keyword default_sort} + Outer_Syntax.local_theory \<^command_keyword>\default_sort\ "declare default sort for explicit type variables" (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy)); val _ = - Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration" + Outer_Syntax.local_theory \<^command_keyword>\typedecl\ "type declaration" (Parse.type_args -- Parse.binding -- Parse.opt_mixfix >> (fn ((args, a), mx) => Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd)); val _ = - Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation" + 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\ @@ -274,11 +274,11 @@ local val _ = - Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment" + Outer_Syntax.command \<^command_keyword>\judgment\ "declare object-logic judgment" (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd)); val _ = - Outer_Syntax.command @{command_keyword consts} "declare constants" + Outer_Syntax.command \<^command_keyword>\consts\ "declare constants" (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd)); in end\ @@ -290,40 +290,40 @@ local val _ = - Outer_Syntax.command @{command_keyword nonterminal} + Outer_Syntax.command \<^command_keyword>\nonterminal\ "declare syntactic type constructors (grammar nonterminal symbols)" (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global)); val _ = - Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses" + Outer_Syntax.command \<^command_keyword>\syntax\ "add raw syntax clauses" (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_syntax_cmd)); val _ = - Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses" + Outer_Syntax.command \<^command_keyword>\no_syntax\ "delete raw syntax clauses" (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_syntax_cmd)); val trans_pat = Scan.optional - (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.name --| @{keyword ")"})) "logic" + (\<^keyword>$\ |-- Parse.!!! (Parse.inner_syntax Parse.name --| \<^keyword>$\)) "logic" -- Parse.inner_syntax Parse.string; fun trans_arrow toks = - ((@{keyword \} || @{keyword =>}) >> K Syntax.Parse_Rule || - (@{keyword \} || @{keyword <=}) >> K Syntax.Print_Rule || - (@{keyword \} || @{keyword ==}) >> K Syntax.Parse_Print_Rule) toks; + ((\<^keyword>\\\ || \<^keyword>\=>\) >> K Syntax.Parse_Rule || + (\<^keyword>\\\ || \<^keyword>\<=\) >> K Syntax.Print_Rule || + (\<^keyword>\\\ || \<^keyword>\==\) >> K Syntax.Parse_Print_Rule) toks; val trans_line = trans_pat -- Parse.!!! (trans_arrow -- trans_pat) >> (fn (left, (arr, right)) => arr (left, right)); val _ = - Outer_Syntax.command @{command_keyword translations} "add syntax translation rules" + Outer_Syntax.command \<^command_keyword>\translations\ "add syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations)); val _ = - Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules" + Outer_Syntax.command \<^command_keyword>\no_translations\ "delete syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations)); in end\ @@ -335,27 +335,27 @@ local val _ = - Outer_Syntax.command @{command_keyword parse_ast_translation} + Outer_Syntax.command \<^command_keyword>\parse_ast_translation\ "install parse ast translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation)); val _ = - Outer_Syntax.command @{command_keyword parse_translation} + Outer_Syntax.command \<^command_keyword>\parse_translation\ "install parse translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation)); val _ = - Outer_Syntax.command @{command_keyword print_translation} + Outer_Syntax.command \<^command_keyword>\print_translation\ "install print translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation)); val _ = - Outer_Syntax.command @{command_keyword typed_print_translation} + Outer_Syntax.command \<^command_keyword>\typed_print_translation\ "install typed print translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation)); val _ = - Outer_Syntax.command @{command_keyword print_ast_translation} + Outer_Syntax.command \<^command_keyword>\print_ast_translation\ "install print ast translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation)); @@ -368,13 +368,13 @@ local val _ = - Outer_Syntax.local_theory' @{command_keyword definition} "constant definition" + Outer_Syntax.local_theory' \<^command_keyword>\definition\ "constant definition" (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) => #2 oo Specification.definition_cmd decl params prems spec)); val _ = - Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation" + Outer_Syntax.local_theory' \<^command_keyword>\abbreviation\ "constant abbreviation" (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec)); @@ -383,19 +383,19 @@ Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a)); val _ = - Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification" + Outer_Syntax.command \<^command_keyword>\axiomatization\ "axiomatic constant specification" (Scan.optional Parse.vars [] -- Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], []) >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d))); val _ = - Outer_Syntax.local_theory @{command_keyword alias} "name-space alias for constant" - (Parse.binding -- (Parse.!!! @{keyword =} |-- Parse.position Parse.name) + Outer_Syntax.local_theory \<^command_keyword>\alias\ "name-space alias for constant" + (Parse.binding -- (Parse.!!! \<^keyword>\=\ |-- Parse.position Parse.name) >> Specification.alias_cmd); val _ = - Outer_Syntax.local_theory @{command_keyword type_alias} "name-space alias for type constructor" - (Parse.binding -- (Parse.!!! @{keyword =} |-- Parse.position Parse.name) + Outer_Syntax.local_theory \<^command_keyword>\type_alias\ "name-space alias for type constructor" + (Parse.binding -- (Parse.!!! \<^keyword>\=\ |-- Parse.position Parse.name) >> Specification.type_alias_cmd); in end\ @@ -407,25 +407,25 @@ local val _ = - Outer_Syntax.local_theory @{command_keyword type_notation} + Outer_Syntax.local_theory \<^command_keyword>\type_notation\ "add concrete syntax for type constructors" (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix) >> (fn (mode, args) => Specification.type_notation_cmd true mode args)); val _ = - Outer_Syntax.local_theory @{command_keyword no_type_notation} + Outer_Syntax.local_theory \<^command_keyword>\no_type_notation\ "delete concrete syntax for type constructors" (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix) >> (fn (mode, args) => Specification.type_notation_cmd false mode args)); val _ = - Outer_Syntax.local_theory @{command_keyword notation} + Outer_Syntax.local_theory \<^command_keyword>\notation\ "add concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Specification.notation_cmd true mode args)); val _ = - Outer_Syntax.local_theory @{command_keyword no_notation} + Outer_Syntax.local_theory \<^command_keyword>\no_notation\ "delete concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Specification.notation_cmd false mode args)); @@ -459,11 +459,11 @@ ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) long Thm.theoremK NONE (K I) binding includes elems concl))); -val _ = theorem @{command_keyword theorem} false "theorem"; -val _ = theorem @{command_keyword lemma} false "lemma"; -val _ = theorem @{command_keyword corollary} false "corollary"; -val _ = theorem @{command_keyword proposition} false "proposition"; -val _ = theorem @{command_keyword schematic_goal} true "schematic goal"; +val _ = theorem \<^command_keyword>\theorem\ false "theorem"; +val _ = theorem \<^command_keyword>\lemma\ false "lemma"; +val _ = theorem \<^command_keyword>\corollary\ false "corollary"; +val _ = theorem \<^command_keyword>\proposition\ false "proposition"; +val _ = theorem \<^command_keyword>\schematic_goal\ true "schematic goal"; in end\ @@ -471,18 +471,18 @@ local val _ = - Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems" + Outer_Syntax.local_theory' \<^command_keyword>\lemmas\ "define theorems" (Parse_Spec.name_facts -- Parse.for_fixes >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes)); val _ = - Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems" + Outer_Syntax.local_theory' \<^command_keyword>\declare\ "declare theorems" (Parse.and_list1 Parse.thms1 -- Parse.for_fixes >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes)); val _ = - Outer_Syntax.local_theory @{command_keyword named_theorems} + Outer_Syntax.local_theory \<^command_keyword>\named_theorems\ "declare named collection of theorems" (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >> fold (fn (b, descr) => snd o Named_Theorems.declare b descr)); @@ -503,19 +503,19 @@ in fold (hide fully o prep ctxt) args thy end)))); val _ = - hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class + hide_names \<^command_keyword>\hide_class\ "classes" Sign.hide_class Parse.class Proof_Context.read_class; val _ = - hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const + hide_names \<^command_keyword>\hide_type\ "types" Sign.hide_type Parse.type_const ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false}); val _ = - hide_names @{command_keyword hide_const} "consts" Sign.hide_const Parse.const + hide_names \<^command_keyword>\hide_const\ "consts" Sign.hide_const Parse.const ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false}); val _ = - hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact + hide_names \<^command_keyword>\hide_fact\ "facts" Global_Theory.hide_fact (Parse.position Parse.name) (Global_Theory.check_fact o Proof_Context.theory_of); in end\ @@ -527,29 +527,29 @@ local val _ = - Outer_Syntax.maybe_begin_local_theory @{command_keyword bundle} + 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} + Outer_Syntax.local_theory \<^command_keyword>\unbundle\