--- 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>\<open>tagged\<close> (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
+ setup \<^binding>\<open>untagged\<close> (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
+ setup \<^binding>\<open>kind\<close> (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
+ setup \<^binding>\<open>THEN\<close>
(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>\<open>OF\<close>
(thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs)))
"rule resolved with facts" #>
- setup @{binding rename_abs}
+ setup \<^binding>\<open>rename_abs\<close>
(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>\<open>unfolded\<close>
(thms >> (fn ths =>
Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths)))
"unfolded definitions" #>
- setup @{binding folded}
+ setup \<^binding>\<open>folded\<close>
(thms >> (fn ths =>
Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths)))
"folded definitions" #>
- setup @{binding consumes}
+ setup \<^binding>\<open>consumes\<close>
(Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
"number of consumed facts" #>
- setup @{binding constraints}
+ setup \<^binding>\<open>constraints\<close>
(Scan.lift Parse.nat >> Rule_Cases.constraints)
"number of equality constraints" #>
- setup @{binding cases_open}
+ setup \<^binding>\<open>cases_open\<close>
(Scan.succeed Rule_Cases.cases_open)
"rule with open parameters" #>
- setup @{binding case_names}
+ setup \<^binding>\<open>case_names\<close>
(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>\<open>case_conclusion\<close>
(Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
"named conclusion of rule cases" #>
- setup @{binding params}
+ setup \<^binding>\<open>params\<close>
(Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
"named rule parameters" #>
- setup @{binding rule_format}
+ setup \<^binding>\<open>rule_format\<close>
(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>\<open>elim_format\<close>
(Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim)))
"destruct rule turned into elimination rule format" #>
- setup @{binding no_vars}
+ setup \<^binding>\<open>no_vars\<close>
(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>\<open>atomize\<close>
(Scan.succeed Object_Logic.declare_atomize) "declaration of atomize rule" #>
- setup @{binding rulify}
+ setup \<^binding>\<open>rulify\<close>
(Scan.succeed Object_Logic.declare_rulify) "declaration of rulify rule" #>
- setup @{binding rotated}
+ setup \<^binding>\<open>rotated\<close>
(Scan.lift (Scan.optional Parse.int 1
>> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))) "rotated theorem premises" #>
- setup @{binding defn}
+ setup \<^binding>\<open>defn\<close>
(add_del Local_Defs.defn_add Local_Defs.defn_del)
"declaration of definitional transformations" #>
- setup @{binding abs_def}
+ setup \<^binding>\<open>abs_def\<close>
(Scan.succeed (Thm.rule_attribute [] (Local_Defs.abs_def_rule o Context.proof_of)))
"abstract over free variables of definitional theorem" #>
--- 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>\<open>trans\<close> (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>\<open>sym\<close> (Attrib.add_del sym_add sym_del)
"declaration of symmetry rule" #>
- Attrib.setup @{binding symmetric} (Scan.succeed symmetric)
+ Attrib.setup \<^binding>\<open>symmetric\<close> (Scan.succeed symmetric)
"resolution with symmetry rule" #>
Global_Theory.add_thms
[((Binding.empty, transitive_thm), [trans_add]),
--- 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>\<open>intro_classes\<close> (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>\<open>standard\<close> (Scan.succeed (METHOD o standard_tac))
"standard proof step: Pure intro/elim rule or class introduction");
--- 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>\<open>codetype\<close>;
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>\<open>code\<close> (Scan.lift code_attribute_parser)
"declare theorems for code generation"
end);
--- 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>\<open>intro\<close> (add intro_bang intro intro_query)
"declaration of introduction rule" #>
- Attrib.setup @{binding elim} (add elim_bang elim elim_query)
+ Attrib.setup \<^binding>\<open>elim\<close> (add elim_bang elim elim_query)
"declaration of elimination rule" #>
- Attrib.setup @{binding dest} (add dest_bang dest dest_query)
+ Attrib.setup \<^binding>\<open>dest\<close> (add dest_bang dest dest_query)
"declaration of destruction rule" #>
- Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
+ Attrib.setup \<^binding>\<open>rule\<close> (Scan.lift Args.del >> K rule_del)
"remove declaration of intro/elim/dest rule");
end;
--- 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>\<open>state\<close>)
(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>\<open>goal\<close>)
(Scan.succeed "Isar_Cmd.diag_goal ML_context"));
--- 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>\<open>intro_locales\<close> (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>\<open>unfold_locales\<close> (Scan.succeed (METHOD o try_intro_locales_tac true))
"back-chain all introduction rules of locales");
--- 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>\<open>rule_trace\<close> (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>\<open>fail\<close> (Scan.succeed (K fail)) "force failure" #>
+ setup \<^binding>\<open>succeed\<close> (Scan.succeed (K succeed)) "succeed" #>
+ setup \<^binding>\<open>sleep\<close> (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>\<open>-\<close> (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>\<open>goal_cases\<close> (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>\<open>insert\<close> (Attrib.thms >> (K o insert))
"insert theorems, ignoring facts" #>
- setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
+ setup \<^binding>\<open>intro\<close> (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>\<open>elim\<close> (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>\<open>unfold\<close> (Attrib.thms >> unfold_meth) "unfold definitions" #>
+ setup \<^binding>\<open>fold\<close> (Attrib.thms >> fold_meth) "fold definitions" #>
+ setup \<^binding>\<open>atomize\<close> (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>\<open>rule\<close> (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>\<open>erule\<close> (xrule_meth erule) "apply rule in elimination manner (improper)" #>
+ setup \<^binding>\<open>drule\<close> (xrule_meth drule) "apply rule in destruct manner (improper)" #>
+ setup \<^binding>\<open>frule\<close> (xrule_meth frule) "apply rule in forward manner (improper)" #>
+ setup \<^binding>\<open>this\<close> (Scan.succeed this) "apply current facts as rules" #>
+ setup \<^binding>\<open>fact\<close> (Attrib.thms >> fact) "composition by facts from context" #>
+ setup \<^binding>\<open>assumption\<close> (Scan.succeed assumption)
"proof by assumption, preferring facts" #>
- setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
+ setup \<^binding>\<open>rename_tac\<close> (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>\<open>rotate_tac\<close> (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>\<open>tactic\<close> (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>\<open>raw_tactic\<close> (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac))
"ML tactic as raw proof method" #>
- setup @{binding use}
+ setup \<^binding>\<open>use\<close>
(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");
--- 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>\<open>show_reverted_improvements\<close> (K true);
fun improve_term_uncheck ts ctxt =
let
--- 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>\<open>undefined\<close>
(Scan.succeed "(raise General.Match)") #>
- ML_Antiquotation.inline @{binding assert}
+ ML_Antiquotation.inline \<^binding>\<open>assert\<close>
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
- ML_Antiquotation.declaration @{binding print}
+ ML_Antiquotation.declaration \<^binding>\<open>print\<close>
(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>\<open>rat\<close>
(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>\<open>system_option\<close>
(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>\<open>theory\<close>
(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>\<open>theory_context\<close>
(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>\<open>context\<close>
(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>\<open>typ\<close> (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
+ ML_Antiquotation.inline \<^binding>\<open>term\<close> (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
+ ML_Antiquotation.inline \<^binding>\<open>prop\<close> (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
- ML_Antiquotation.value @{binding ctyp} (Args.typ >> (fn T =>
+ ML_Antiquotation.value \<^binding>\<open>ctyp\<close> (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>\<open>cterm\<close> (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>\<open>cprop\<close> (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>\<open>method\<close>
(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>\<open>locale\<close>
(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>\<open>class\<close> (class false) #>
+ ML_Antiquotation.inline \<^binding>\<open>class_syntax\<close> (class true) #>
- ML_Antiquotation.inline @{binding sort}
+ ML_Antiquotation.inline \<^binding>\<open>sort\<close>
(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>\<open>type_name\<close>
(type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
- ML_Antiquotation.inline @{binding type_abbrev}
+ ML_Antiquotation.inline \<^binding>\<open>type_abbrev\<close>
(type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
- ML_Antiquotation.inline @{binding nonterminal}
+ ML_Antiquotation.inline \<^binding>\<open>nonterminal\<close>
(type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
- ML_Antiquotation.inline @{binding type_syntax}
+ ML_Antiquotation.inline \<^binding>\<open>type_syntax\<close>
(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>\<open>const_name\<close>
(const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
- ML_Antiquotation.inline @{binding const_abbrev}
+ ML_Antiquotation.inline \<^binding>\<open>const_abbrev\<close>
(const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
- ML_Antiquotation.inline @{binding const_syntax}
+ ML_Antiquotation.inline \<^binding>\<open>const_syntax\<close>
(const_name (fn (_, c) => Lexicon.mark_const c)) #>
- ML_Antiquotation.inline @{binding syntax_const}
+ ML_Antiquotation.inline \<^binding>\<open>syntax_const\<close>
(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>\<open>const\<close>
(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>\<open>map\<close>
(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>\<open>fold\<close>
(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>\<open>fold_map\<close>
(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>\<open>split_list\<close>
(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>\<open>apply\<close>
(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>\<open>keyword\<close>
(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>\<open>command_keyword\<close>
(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 =>
--- 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>\<open>attributes\<close> 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>\<open>thm\<close> (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
+ ML_Antiquotation.declaration \<^binding>\<open>thms\<close> 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>\<open>lemma\<close>
(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 =>
--- 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 @@
\<close>
\<close>
-ML \<open>@{assert} (not (can ML \<open>open RunCall\<close>))\<close>
+ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close>
subsection \<open>Switch to bootstrap environment\<close>
--- 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>\<open>path\<close> (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>\<open>file\<close> (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>\<open>dir\<close> (Scan.lift (Parse.position Parse.path))
(document_antiq (SOME File.check_dir) o #context) #>
- ML_Antiquotation.value @{binding path}
+ ML_Antiquotation.value \<^binding>\<open>path\<close>
(Args.context -- Scan.lift (Parse.position Parse.path)
>> uncurry (ML_antiq NONE)) #>
- ML_Antiquotation.value @{binding file}
+ ML_Antiquotation.value \<^binding>\<open>file\<close>
(Args.context -- Scan.lift (Parse.position Parse.path)
>> uncurry (ML_antiq (SOME File.check_file))) #>
- ML_Antiquotation.value @{binding dir}
+ ML_Antiquotation.value \<^binding>\<open>dir\<close>
(Args.context -- Scan.lift (Parse.position Parse.path)
>> uncurry (ML_antiq (SOME File.check_dir))));
--- 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>\<open>extraction_expand\<close> (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>\<open>extraction_expand_def\<close> (Scan.succeed (extraction_expand true))
"specify definitions to be expanded during extraction");
--- 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 \<open>External file dependencies\<close>
ML \<open>
- Outer_Syntax.command @{command_keyword external_file} "formal dependency on external file"
+ Outer_Syntax.command \<^command_keyword>\<open>external_file\<close> "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 \<open>
local
-val semi = Scan.option @{keyword ";"};
+val semi = Scan.option \<^keyword>\<open>;\<close>;
val _ =
- Outer_Syntax.command @{command_keyword ML_file} "read and evaluate Isabelle/ML file"
+ Outer_Syntax.command \<^command_keyword>\<open>ML_file\<close> "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>\<open>ML_file_debug\<close>
"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>\<open>ML_file_no_debug\<close>
"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>\<open>SML_file\<close> "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>\<open>SML_file_debug\<close>
"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>\<open>SML_file_no_debug\<close>
"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>\<open>SML_export\<close> "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>\<open>SML_import\<close> "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>\<open>ML_prf\<close> "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>\<open>ML_val\<close> "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>\<open>ML_command\<close> "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>\<open>setup\<close> "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>\<open>local_setup\<close> "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>\<open>oracle\<close> "declare oracle"
+ (Parse.range Parse.name -- (\<^keyword>\<open>=\<close> |-- 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>\<open>attribute_setup\<close> "define attribute in ML"
(Parse.position Parse.name --
- Parse.!!! (@{keyword =} |-- Parse.ML_source -- Scan.optional Parse.text "")
+ Parse.!!! (\<^keyword>\<open>=\<close> |-- 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>\<open>method_setup\<close> "define proof method in ML"
(Parse.position Parse.name --
- Parse.!!! (@{keyword =} |-- Parse.ML_source -- Scan.optional Parse.text "")
+ Parse.!!! (\<^keyword>\<open>=\<close> |-- 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>\<open>declaration\<close> "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>\<open>syntax_declaration\<close> "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>\<open>simproc_setup\<close> "define simproc in ML"
(Parse.position Parse.name --
- (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword =}) --
+ (\<^keyword>\<open>(\<close> |-- Parse.enum1 "|" Parse.term --| \<^keyword>\<open>)\<close> --| \<^keyword>\<open>=\<close>) --
Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c));
in end\<close>
@@ -249,20 +249,20 @@
local
val _ =
- Outer_Syntax.local_theory @{command_keyword default_sort}
+ Outer_Syntax.local_theory \<^command_keyword>\<open>default_sort\<close>
"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>\<open>typedecl\<close> "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>\<open>type_synonym\<close> "declare type abbreviation"
(Parse.type_args -- Parse.binding --
- (@{keyword =} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
+ (\<^keyword>\<open>=\<close> |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
>> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
in end\<close>
@@ -274,11 +274,11 @@
local
val _ =
- Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment"
+ Outer_Syntax.command \<^command_keyword>\<open>judgment\<close> "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>\<open>consts\<close> "declare constants"
(Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
in end\<close>
@@ -290,40 +290,40 @@
local
val _ =
- Outer_Syntax.command @{command_keyword nonterminal}
+ Outer_Syntax.command \<^command_keyword>\<open>nonterminal\<close>
"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>\<open>syntax\<close> "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>\<open>no_syntax\<close> "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>\<open>(\<close> |-- Parse.!!! (Parse.inner_syntax Parse.name --| \<^keyword>\<open>)\<close>)) "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>\<open>\<rightharpoonup>\<close> || \<^keyword>\<open>=>\<close>) >> K Syntax.Parse_Rule ||
+ (\<^keyword>\<open>\<leftharpoondown>\<close> || \<^keyword>\<open><=\<close>) >> K Syntax.Print_Rule ||
+ (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>) >> 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>\<open>translations\<close> "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>\<open>no_translations\<close> "delete syntax translation rules"
(Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
in end\<close>
@@ -335,27 +335,27 @@
local
val _ =
- Outer_Syntax.command @{command_keyword parse_ast_translation}
+ Outer_Syntax.command \<^command_keyword>\<open>parse_ast_translation\<close>
"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>\<open>parse_translation\<close>
"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>\<open>print_translation\<close>
"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>\<open>typed_print_translation\<close>
"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>\<open>print_ast_translation\<close>
"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>\<open>definition\<close> "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>\<open>abbreviation\<close> "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>\<open>axiomatization\<close> "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>\<open>alias\<close> "name-space alias for constant"
+ (Parse.binding -- (Parse.!!! \<^keyword>\<open>=\<close> |-- 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>\<open>type_alias\<close> "name-space alias for type constructor"
+ (Parse.binding -- (Parse.!!! \<^keyword>\<open>=\<close> |-- Parse.position Parse.name)
>> Specification.type_alias_cmd);
in end\<close>
@@ -407,25 +407,25 @@
local
val _ =
- Outer_Syntax.local_theory @{command_keyword type_notation}
+ Outer_Syntax.local_theory \<^command_keyword>\<open>type_notation\<close>
"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>\<open>no_type_notation\<close>
"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>\<open>notation\<close>
"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>\<open>no_notation\<close>
"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>\<open>theorem\<close> false "theorem";
+val _ = theorem \<^command_keyword>\<open>lemma\<close> false "lemma";
+val _ = theorem \<^command_keyword>\<open>corollary\<close> false "corollary";
+val _ = theorem \<^command_keyword>\<open>proposition\<close> false "proposition";
+val _ = theorem \<^command_keyword>\<open>schematic_goal\<close> true "schematic goal";
in end\<close>
@@ -471,18 +471,18 @@
local
val _ =
- Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
+ Outer_Syntax.local_theory' \<^command_keyword>\<open>lemmas\<close> "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>\<open>declare\<close> "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>\<open>named_theorems\<close>
"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>\<open>hide_class\<close> "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>\<open>hide_type\<close> "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>\<open>hide_const\<close> "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>\<open>hide_fact\<close> "facts" Global_Theory.hide_fact
(Parse.position Parse.name) (Global_Theory.check_fact o Proof_Context.theory_of);
in end\<close>
@@ -527,29 +527,29 @@
local
val _ =
- Outer_Syntax.maybe_begin_local_theory @{command_keyword bundle}
+ Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\<open>bundle\<close>
"define bundle of declarations"
- ((Parse.binding --| @{keyword =}) -- Parse.thms1 -- Parse.for_fixes
+ ((Parse.binding --| \<^keyword>\<open>=\<close>) -- 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>\<open>unbundle\<close>
"activate declarations from bundle in local theory"
(Scan.repeat1 (Parse.position Parse.name) >> Bundle.unbundle_cmd);
val _ =
- Outer_Syntax.command @{command_keyword include}
+ Outer_Syntax.command \<^command_keyword>\<open>include\<close>
"activate declarations from bundle in proof body"
(Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd));
val _ =
- Outer_Syntax.command @{command_keyword including}
+ Outer_Syntax.command \<^command_keyword>\<open>including\<close>
"activate declarations from bundle in goal refinement"
(Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.including_cmd));
val _ =
- Outer_Syntax.command @{command_keyword print_bundles}
+ Outer_Syntax.command \<^command_keyword>\<open>print_bundles\<close>
"print bundles of declarations"
(Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
@@ -564,7 +564,7 @@
local
val _ =
- Outer_Syntax.command @{command_keyword context} "begin local theory context"
+ Outer_Syntax.command \<^command_keyword>\<open>context\<close> "begin local theory context"
((Parse.position Parse.name >> (fn name =>
Toplevel.begin_local_theory true (Named_Target.begin name)) ||
Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
@@ -572,7 +572,7 @@
--| Parse.begin);
val _ =
- Outer_Syntax.command @{command_keyword end} "end context"
+ Outer_Syntax.command \<^command_keyword>\<open>end\<close> "end context"
(Scan.succeed
(Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
Toplevel.end_proof (K Proof.end_notepad)));
@@ -587,19 +587,19 @@
val locale_val =
Parse_Spec.locale_expression --
- Scan.optional (@{keyword +} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
+ Scan.optional (\<^keyword>\<open>+\<close> |-- 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"
+ Outer_Syntax.command \<^command_keyword>\<open>locale\<close> "define named specification context"
(Parse.binding --
- Scan.optional (@{keyword =} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
+ Scan.optional (\<^keyword>\<open>=\<close> |-- 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 _ =
- Outer_Syntax.command @{command_keyword experiment} "open private specification context"
+ Outer_Syntax.command \<^command_keyword>\<open>experiment\<close> "open private specification context"
(Scan.repeat Parse_Spec.context_element --| Parse.begin
>> (fn elems =>
Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
@@ -607,38 +607,38 @@
val interpretation_args =
Parse.!!! Parse_Spec.locale_expression --
Scan.optional
- (@{keyword rewrites} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
+ (\<^keyword>\<open>rewrites\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
val _ =
- Outer_Syntax.command @{command_keyword interpret}
+ Outer_Syntax.command \<^command_keyword>\<open>interpret\<close>
"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>\<open>defines\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+ -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))) [] --
Scan.optional
- (@{keyword rewrites} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
+ (\<^keyword>\<open>rewrites\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
val _ =
- Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation}
+ Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretation\<close>
"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}
+ Outer_Syntax.command \<^command_keyword>\<open>sublocale\<close>
"prove sublocale relation between a locale and a locale expression"
- ((Parse.position Parse.name --| (@{keyword \<subseteq>} || @{keyword <}) --
+ ((Parse.position Parse.name --| (\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) --
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)));
val _ =
- Outer_Syntax.command @{command_keyword interpretation}
+ Outer_Syntax.command \<^command_keyword>\<open>interpretation\<close>
"prove interpretation of locale expression in local theory or into global theory"
(interpretation_args >> (fn (expr, equations) =>
Toplevel.local_theory_to_proof NONE NONE
@@ -654,29 +654,29 @@
val class_val =
Parse_Spec.class_expression --
- Scan.optional (@{keyword +} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
+ Scan.optional (\<^keyword>\<open>+\<close> |-- 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
+ Outer_Syntax.command \<^command_keyword>\<open>class\<close> "define type class"
+ (Parse.binding -- Scan.optional (\<^keyword>\<open>=\<close> |-- class_val) ([], []) -- Parse.opt_begin
>> (fn ((name, (supclasses, elems)), begin) =>
Toplevel.begin_local_theory begin
(Class_Declaration.class_cmd name supclasses elems #> snd)));
val _ =
- Outer_Syntax.local_theory_to_proof @{command_keyword subclass} "prove a subclass relation"
+ Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>subclass\<close> "prove a subclass relation"
(Parse.class >> Class_Declaration.subclass_cmd);
val _ =
- Outer_Syntax.command @{command_keyword instantiation} "instantiate and prove type arity"
+ Outer_Syntax.command \<^command_keyword>\<open>instantiation\<close> "instantiate and prove type arity"
(Parse.multi_arity --| Parse.begin
>> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
val _ =
- Outer_Syntax.command @{command_keyword instance} "prove type arity or subclass relation"
+ Outer_Syntax.command \<^command_keyword>\<open>instance\<close> "prove type arity or subclass relation"
((Parse.class --
- ((@{keyword \<subseteq>} || @{keyword <}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
+ ((\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) |-- 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)));
@@ -689,9 +689,9 @@
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
+ Outer_Syntax.command \<^command_keyword>\<open>overloading\<close> "overloaded definitions"
+ (Scan.repeat1 (Parse.name --| (\<^keyword>\<open>==\<close> || \<^keyword>\<open>\<equiv>\<close>) -- Parse.term --
+ Scan.optional (\<^keyword>\<open>(\<close> |-- (\<^keyword>\<open>unchecked\<close> >> K false) --| \<^keyword>\<open>)\<close>) true
>> Scan.triple1) --| Parse.begin
>> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
@@ -704,7 +704,7 @@
local
val _ =
- Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
+ Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>notepad\<close> "begin proof context"
(Parse.begin >> K Proof.begin_notepad);
in end\<close>
@@ -720,22 +720,22 @@
>> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
val _ =
- Outer_Syntax.command @{command_keyword have} "state local goal"
+ Outer_Syntax.command \<^command_keyword>\<open>have\<close> "state local goal"
(structured_statement >> (fn (a, b, c, d) =>
Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2)));
val _ =
- Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals"
+ Outer_Syntax.command \<^command_keyword>\<open>show\<close> "state local goal, to refine pending subgoals"
(structured_statement >> (fn (a, b, c, d) =>
Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2)));
val _ =
- Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
+ Outer_Syntax.command \<^command_keyword>\<open>hence\<close> "old-style alias of \"then have\""
(structured_statement >> (fn (a, b, c, d) =>
Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2)));
val _ =
- Outer_Syntax.command @{command_keyword thus} "old-style alias of \"then show\""
+ Outer_Syntax.command \<^command_keyword>\<open>thus\<close> "old-style alias of \"then show\""
(structured_statement >> (fn (a, b, c, d) =>
Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2)));
@@ -750,31 +750,31 @@
val facts = Parse.and_list1 Parse.thms1;
val _ =
- Outer_Syntax.command @{command_keyword then} "forward chaining"
+ Outer_Syntax.command \<^command_keyword>\<open>then\<close> "forward chaining"
(Scan.succeed (Toplevel.proof Proof.chain));
val _ =
- Outer_Syntax.command @{command_keyword from} "forward chaining from given facts"
+ Outer_Syntax.command \<^command_keyword>\<open>from\<close> "forward chaining from given facts"
(facts >> (Toplevel.proof o Proof.from_thmss_cmd));
val _ =
- Outer_Syntax.command @{command_keyword with} "forward chaining from given and current facts"
+ Outer_Syntax.command \<^command_keyword>\<open>with\<close> "forward chaining from given and current facts"
(facts >> (Toplevel.proof o Proof.with_thmss_cmd));
val _ =
- Outer_Syntax.command @{command_keyword note} "define facts"
+ Outer_Syntax.command \<^command_keyword>\<open>note\<close> "define facts"
(Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
val _ =
- Outer_Syntax.command @{command_keyword supply} "define facts during goal refinement (unstructured)"
+ Outer_Syntax.command \<^command_keyword>\<open>supply\<close> "define facts during goal refinement (unstructured)"
(Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd));
val _ =
- Outer_Syntax.command @{command_keyword using} "augment goal facts"
+ Outer_Syntax.command \<^command_keyword>\<open>using\<close> "augment goal facts"
(facts >> (Toplevel.proof o Proof.using_cmd));
val _ =
- Outer_Syntax.command @{command_keyword unfolding} "unfold definitions in goal and facts"
+ Outer_Syntax.command \<^command_keyword>\<open>unfolding\<close> "unfold definitions in goal and facts"
(facts >> (Toplevel.proof o Proof.unfolding_cmd));
in end\<close>
@@ -790,51 +790,51 @@
>> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
val _ =
- Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)"
+ Outer_Syntax.command \<^command_keyword>\<open>fix\<close> "fix local variables (Skolem constants)"
(Parse.vars >> (Toplevel.proof o Proof.fix_cmd));
val _ =
- Outer_Syntax.command @{command_keyword assume} "assume propositions"
+ Outer_Syntax.command \<^command_keyword>\<open>assume\<close> "assume propositions"
(structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c)));
val _ =
- Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later"
+ Outer_Syntax.command \<^command_keyword>\<open>presume\<close> "assume propositions, to be established later"
(structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
val _ =
- Outer_Syntax.command @{command_keyword define} "local definition (non-polymorphic)"
+ Outer_Syntax.command \<^command_keyword>\<open>define\<close> "local definition (non-polymorphic)"
((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
>> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
val _ =
- Outer_Syntax.command @{command_keyword consider} "state cases rule"
+ Outer_Syntax.command \<^command_keyword>\<open>consider\<close> "state cases rule"
(Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));
val _ =
- Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
+ Outer_Syntax.command \<^command_keyword>\<open>obtain\<close> "generalized elimination"
(Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement
>> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
val _ =
- Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
+ Outer_Syntax.command \<^command_keyword>\<open>guess\<close> "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))
+ Outer_Syntax.command \<^command_keyword>\<open>let\<close> "bind text variables"
+ (Parse.and_list1 (Parse.and_list1 Parse.term -- (\<^keyword>\<open>=\<close> |-- Parse.term))
>> (Toplevel.proof o Proof.let_bind_cmd));
val _ =
- Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables"
+ Outer_Syntax.command \<^command_keyword>\<open>write\<close> "add concrete syntax for constants / fixed variables"
(Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
>> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
val _ =
- Outer_Syntax.command @{command_keyword case} "invoke local context"
+ Outer_Syntax.command \<^command_keyword>\<open>case\<close> "invoke local context"
(Parse_Spec.opt_thm_name ":" --
- (@{keyword "("} |--
+ (\<^keyword>\<open>(\<close> |--
Parse.!!! (Parse.position Parse.name -- Scan.repeat (Parse.maybe Parse.binding)
- --| @{keyword ")"}) ||
+ --| \<^keyword>\<open>)\<close>) ||
Parse.position Parse.name >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
in end\<close>
@@ -846,15 +846,15 @@
local
val _ =
- Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block"
+ Outer_Syntax.command \<^command_keyword>\<open>{\<close> "begin explicit proof block"
(Scan.succeed (Toplevel.proof Proof.begin_block));
val _ =
- Outer_Syntax.command @{command_keyword "}"} "end explicit proof block"
+ Outer_Syntax.command \<^command_keyword>\<open>}\<close> "end explicit proof block"
(Scan.succeed (Toplevel.proof Proof.end_block));
val _ =
- Outer_Syntax.command @{command_keyword next} "enter next proof block"
+ Outer_Syntax.command \<^command_keyword>\<open>next\<close> "enter next proof block"
(Scan.succeed (Toplevel.proof Proof.next_block));
in end\<close>
@@ -866,40 +866,40 @@
local
val _ =
- Outer_Syntax.command @{command_keyword qed} "conclude proof"
+ Outer_Syntax.command \<^command_keyword>\<open>qed\<close> "conclude proof"
(Scan.option Method.parse >> (fn m =>
(Option.map Method.report m;
Isar_Cmd.qed m)));
val _ =
- Outer_Syntax.command @{command_keyword by} "terminal backward proof"
+ Outer_Syntax.command \<^command_keyword>\<open>by\<close> "terminal backward proof"
(Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
(Method.report m1;
Option.map Method.report m2;
Isar_Cmd.terminal_proof (m1, m2))));
val _ =
- Outer_Syntax.command @{command_keyword ".."} "default proof"
+ Outer_Syntax.command \<^command_keyword>\<open>..\<close> "default proof"
(Scan.succeed Isar_Cmd.default_proof);
val _ =
- Outer_Syntax.command @{command_keyword "."} "immediate proof"
+ Outer_Syntax.command \<^command_keyword>\<open>.\<close> "immediate proof"
(Scan.succeed Isar_Cmd.immediate_proof);
val _ =
- Outer_Syntax.command @{command_keyword done} "done proof"
+ Outer_Syntax.command \<^command_keyword>\<open>done\<close> "done proof"
(Scan.succeed Isar_Cmd.done_proof);
val _ =
- Outer_Syntax.command @{command_keyword sorry} "skip proof (quick-and-dirty mode only!)"
+ Outer_Syntax.command \<^command_keyword>\<open>sorry\<close> "skip proof (quick-and-dirty mode only!)"
(Scan.succeed Isar_Cmd.skip_proof);
val _ =
- Outer_Syntax.command @{command_keyword \<proof>} "dummy proof (quick-and-dirty mode only!)"
+ Outer_Syntax.command \<^command_keyword>\<open>\<proof>\<close> "dummy proof (quick-and-dirty mode only!)"
(Scan.succeed Isar_Cmd.skip_proof);
val _ =
- Outer_Syntax.command @{command_keyword oops} "forget proof"
+ Outer_Syntax.command \<^command_keyword>\<open>oops\<close> "forget proof"
(Scan.succeed (Toplevel.forget_proof true));
in end\<close>
@@ -911,23 +911,23 @@
local
val _ =
- Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state"
+ Outer_Syntax.command \<^command_keyword>\<open>defer\<close> "shuffle internal proof state"
(Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
val _ =
- Outer_Syntax.command @{command_keyword prefer} "shuffle internal proof state"
+ Outer_Syntax.command \<^command_keyword>\<open>prefer\<close> "shuffle internal proof state"
(Parse.nat >> (Toplevel.proof o Proof.prefer));
val _ =
- Outer_Syntax.command @{command_keyword apply} "initial goal refinement step (unstructured)"
+ Outer_Syntax.command \<^command_keyword>\<open>apply\<close> "initial goal refinement step (unstructured)"
(Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m))));
val _ =
- Outer_Syntax.command @{command_keyword apply_end} "terminal goal refinement step (unstructured)"
+ Outer_Syntax.command \<^command_keyword>\<open>apply_end\<close> "terminal goal refinement step (unstructured)"
(Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m))));
val _ =
- Outer_Syntax.command @{command_keyword proof} "backward proof step"
+ Outer_Syntax.command \<^command_keyword>\<open>proof\<close> "backward proof step"
(Scan.option Method.parse >> (fn m =>
(Option.map Method.report m;
Toplevel.proof (fn state =>
@@ -952,15 +952,15 @@
val for_params =
Scan.optional
- (@{keyword for} |--
+ (\<^keyword>\<open>for\<close> |--
Parse.!!! ((Scan.option Parse.dots >> is_some) --
(Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
(false, []);
val _ =
- Outer_Syntax.command @{command_keyword subgoal}
+ Outer_Syntax.command \<^command_keyword>\<open>subgoal\<close>
"focus on first subgoal within backward refinement"
- (opt_fact_binding -- (Scan.option (@{keyword premises} |-- Parse.!!! opt_fact_binding)) --
+ (opt_fact_binding -- (Scan.option (\<^keyword>\<open>premises\<close> |-- 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)));
@@ -973,28 +973,28 @@
local
val calculation_args =
- Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.thms1 --| @{keyword ")"})));
+ Scan.option (\<^keyword>\<open>(\<close> |-- Parse.!!! ((Parse.thms1 --| \<^keyword>\<open>)\<close>)));
val _ =
- Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
+ Outer_Syntax.command \<^command_keyword>\<open>also\<close> "combine calculation and current facts"
(calculation_args >> (Toplevel.proofs' o Calculation.also_cmd));
val _ =
- Outer_Syntax.command @{command_keyword finally}
+ Outer_Syntax.command \<^command_keyword>\<open>finally\<close>
"combine calculation and current facts, exhibit result"
(calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd));
val _ =
- Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts"
+ Outer_Syntax.command \<^command_keyword>\<open>moreover\<close> "augment calculation by current facts"
(Scan.succeed (Toplevel.proof' Calculation.moreover));
val _ =
- Outer_Syntax.command @{command_keyword ultimately}
+ Outer_Syntax.command \<^command_keyword>\<open>ultimately\<close>
"augment calculation by current facts, exhibit result"
(Scan.succeed (Toplevel.proof' Calculation.ultimately));
val _ =
- Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
+ Outer_Syntax.command \<^command_keyword>\<open>print_trans_rules\<close> "print transitivity rules"
(Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
in end\<close>
@@ -1009,7 +1009,7 @@
Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"];
val _ =
- Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
+ Outer_Syntax.command \<^command_keyword>\<open>back\<close> "explicit backtracking of proof command"
(Scan.succeed
(Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
Toplevel.skip_proof report_back));
@@ -1023,123 +1023,123 @@
local
val opt_modes =
- Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
+ Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\<open>)\<close>)) [];
val _ =
- Outer_Syntax.command @{command_keyword help}
+ Outer_Syntax.command \<^command_keyword>\<open>help\<close>
"retrieve outer syntax commands according to name patterns"
(Scan.repeat Parse.name >>
(fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats)));
val _ =
- Outer_Syntax.command @{command_keyword print_commands} "print outer syntax commands"
+ Outer_Syntax.command \<^command_keyword>\<open>print_commands\<close> "print outer syntax commands"
(Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_options} "print configuration options"
+ Outer_Syntax.command \<^command_keyword>\<open>print_options\<close> "print configuration options"
(Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_context}
+ Outer_Syntax.command \<^command_keyword>\<open>print_context\<close>
"print context of local theory target"
(Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
val _ =
- Outer_Syntax.command @{command_keyword print_theory}
+ Outer_Syntax.command \<^command_keyword>\<open>print_theory\<close>
"print logical theory contents"
(Parse.opt_bang >> (fn b =>
Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_definitions}
+ Outer_Syntax.command \<^command_keyword>\<open>print_definitions\<close>
"print dependencies of definitional theory content"
(Parse.opt_bang >> (fn b =>
Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_syntax}
+ Outer_Syntax.command \<^command_keyword>\<open>print_syntax\<close>
"print inner syntax of context"
(Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_defn_rules}
+ Outer_Syntax.command \<^command_keyword>\<open>print_defn_rules\<close>
"print definitional rewrite rules of context"
(Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_abbrevs}
+ Outer_Syntax.command \<^command_keyword>\<open>print_abbrevs\<close>
"print constant abbreviations of context"
(Parse.opt_bang >> (fn b =>
Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_theorems}
+ Outer_Syntax.command \<^command_keyword>\<open>print_theorems\<close>
"print theorems of local theory or proof context"
(Parse.opt_bang >> (fn b =>
Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
val _ =
- Outer_Syntax.command @{command_keyword print_locales}
+ Outer_Syntax.command \<^command_keyword>\<open>print_locales\<close>
"print locales of this theory"
(Parse.opt_bang >> (fn b =>
Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_classes}
+ Outer_Syntax.command \<^command_keyword>\<open>print_classes\<close>
"print classes of this theory"
(Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_locale}
+ Outer_Syntax.command \<^command_keyword>\<open>print_locale\<close>
"print locale of this theory"
(Parse.opt_bang -- Parse.position Parse.name >> (fn (b, name) =>
Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
val _ =
- Outer_Syntax.command @{command_keyword print_interps}
+ Outer_Syntax.command \<^command_keyword>\<open>print_interps\<close>
"print interpretations of locale for this theory or proof context"
(Parse.position Parse.name >> (fn name =>
Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
val _ =
- Outer_Syntax.command @{command_keyword print_dependencies}
+ Outer_Syntax.command \<^command_keyword>\<open>print_dependencies\<close>
"print dependencies of locale expression"
(Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (b, expr) =>
Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
val _ =
- Outer_Syntax.command @{command_keyword print_attributes}
+ Outer_Syntax.command \<^command_keyword>\<open>print_attributes\<close>
"print attributes of this theory"
(Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_simpset}
+ Outer_Syntax.command \<^command_keyword>\<open>print_simpset\<close>
"print context of Simplifier"
(Parse.opt_bang >> (fn b =>
Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules"
+ Outer_Syntax.command \<^command_keyword>\<open>print_rules\<close> "print intro/elim rules"
(Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory"
+ Outer_Syntax.command \<^command_keyword>\<open>print_methods\<close> "print methods of this theory"
(Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_antiquotations}
+ Outer_Syntax.command \<^command_keyword>\<open>print_antiquotations\<close>
"print document antiquotations"
(Parse.opt_bang >> (fn b =>
Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_ML_antiquotations}
+ Outer_Syntax.command \<^command_keyword>\<open>print_ML_antiquotations\<close>
"print ML antiquotations"
(Parse.opt_bang >> (fn b =>
Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
+ Outer_Syntax.command \<^command_keyword>\<open>locale_deps\<close> "visualize locale dependencies"
(Scan.succeed
(Toplevel.keep (Toplevel.theory_of #> (fn thy =>
Locale.pretty_locale_deps thy
@@ -1148,68 +1148,68 @@
|> Graph_Display.display_graph_old))));
val _ =
- Outer_Syntax.command @{command_keyword print_term_bindings}
+ Outer_Syntax.command \<^command_keyword>\<open>print_term_bindings\<close>
"print term bindings of proof context"
(Scan.succeed
(Toplevel.keep
(Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context"
+ Outer_Syntax.command \<^command_keyword>\<open>print_facts\<close> "print facts of proof context"
(Parse.opt_bang >> (fn b =>
Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context"
+ Outer_Syntax.command \<^command_keyword>\<open>print_cases\<close> "print cases of proof context"
(Scan.succeed
(Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_statement}
+ Outer_Syntax.command \<^command_keyword>\<open>print_statement\<close>
"print theorems as long statements"
(opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts);
val _ =
- Outer_Syntax.command @{command_keyword thm} "print theorems"
+ Outer_Syntax.command \<^command_keyword>\<open>thm\<close> "print theorems"
(opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms);
val _ =
- Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
+ Outer_Syntax.command \<^command_keyword>\<open>prf\<close> "print proof terms of theorems"
(opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false);
val _ =
- Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
+ Outer_Syntax.command \<^command_keyword>\<open>full_prf\<close> "print full proof terms of theorems"
(opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true);
val _ =
- Outer_Syntax.command @{command_keyword prop} "read and print proposition"
+ Outer_Syntax.command \<^command_keyword>\<open>prop\<close> "read and print proposition"
(opt_modes -- Parse.term >> Isar_Cmd.print_prop);
val _ =
- Outer_Syntax.command @{command_keyword term} "read and print term"
+ Outer_Syntax.command \<^command_keyword>\<open>term\<close> "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))
+ Outer_Syntax.command \<^command_keyword>\<open>typ\<close> "read and print type"
+ (opt_modes -- (Parse.typ -- Scan.option (\<^keyword>\<open>::\<close> |-- Parse.!!! Parse.sort))
>> Isar_Cmd.print_type);
val _ =
- Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
+ Outer_Syntax.command \<^command_keyword>\<open>print_codesetup\<close> "print code generator setup"
(Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
val _ =
- Outer_Syntax.command @{command_keyword print_state}
+ Outer_Syntax.command \<^command_keyword>\<open>print_state\<close>
"print current proof state (if present)"
(opt_modes >> (fn modes =>
Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state))));
val _ =
- Outer_Syntax.command @{command_keyword welcome} "print welcome message"
+ Outer_Syntax.command \<^command_keyword>\<open>welcome\<close> "print welcome message"
(Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ()))));
val _ =
- Outer_Syntax.command @{command_keyword display_drafts}
+ Outer_Syntax.command \<^command_keyword>\<open>display_drafts\<close>
"display raw source files with symbols"
(Scan.repeat1 Parse.path >> (fn names =>
Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
@@ -1224,26 +1224,26 @@
val theory_bounds =
Parse.position Parse.theory_name >> single ||
- (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_name) --| @{keyword ")"});
+ (\<^keyword>\<open>(\<close> |-- Parse.enum "|" (Parse.position Parse.theory_name) --| \<^keyword>\<open>)\<close>);
val _ =
- Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
+ Outer_Syntax.command \<^command_keyword>\<open>thy_deps\<close> "visualize theory dependencies"
(Scan.option theory_bounds -- Scan.option theory_bounds >>
(fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args)));
val class_bounds =
Parse.sort >> single ||
- (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
+ (\<^keyword>\<open>(\<close> |-- Parse.enum "|" Parse.sort --| \<^keyword>\<open>)\<close>);
val _ =
- Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
+ Outer_Syntax.command \<^command_keyword>\<open>class_deps\<close> "visualize class dependencies"
(Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args)));
val _ =
- Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
+ Outer_Syntax.command \<^command_keyword>\<open>thm_deps\<close> "visualize theorem dependencies"
(Parse.thms1 >> (fn args =>
Toplevel.keep (fn st =>
Thm_Deps.thm_deps (Toplevel.theory_of st)
@@ -1254,7 +1254,7 @@
Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name));
val _ =
- Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
+ Outer_Syntax.command \<^command_keyword>\<open>unused_thms\<close> "find unused theorems"
(Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
Toplevel.keep (fn st =>
let
@@ -1280,7 +1280,7 @@
local
val _ =
- Outer_Syntax.command @{command_keyword find_consts}
+ Outer_Syntax.command \<^command_keyword>\<open>find_consts\<close>
"find constants by name / type patterns"
(Find_Consts.query_parser >> (fn spec =>
Toplevel.keep (fn st =>
@@ -1294,7 +1294,7 @@
(NONE, true);
val _ =
- Outer_Syntax.command @{command_keyword find_theorems}
+ Outer_Syntax.command \<^command_keyword>\<open>find_theorems\<close>
"find theorems meeting specified criteria"
(options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) =>
Toplevel.keep (fn st =>
@@ -1310,7 +1310,7 @@
local
val _ =
- Outer_Syntax.command @{command_keyword code_datatype}
+ Outer_Syntax.command \<^command_keyword>\<open>code_datatype\<close>
"define set of code datatype constructors"
(Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd));
@@ -1325,24 +1325,24 @@
val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
val _ =
- Outer_Syntax.command @{command_keyword realizers}
+ Outer_Syntax.command \<^command_keyword>\<open>realizers\<close>
"specify realizers for primitive axioms / theorems, together with correctness proof"
(Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
(fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
(map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
val _ =
- Outer_Syntax.command @{command_keyword realizability}
+ Outer_Syntax.command \<^command_keyword>\<open>realizability\<close>
"add equations characterizing realizability"
(Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
val _ =
- Outer_Syntax.command @{command_keyword extract_type}
+ Outer_Syntax.command \<^command_keyword>\<open>extract_type\<close>
"add equations characterizing type of extracted program"
(Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
val _ =
- Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
+ Outer_Syntax.command \<^command_keyword>\<open>extract\<close> "extract terms from proofs"
(Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
--- a/src/Pure/Thy/document_antiquotations.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Wed Dec 06 18:59:33 2017 +0100
@@ -21,9 +21,9 @@
val _ =
Theory.setup
- (markdown_error @{binding item} #>
- markdown_error @{binding enum} #>
- markdown_error @{binding descr});
+ (markdown_error \<^binding>\<open>item\<close> #>
+ markdown_error \<^binding>\<open>enum\<close> #>
+ markdown_error \<^binding>\<open>descr\<close>);
end;
@@ -32,10 +32,10 @@
val _ =
Theory.setup
- (Thy_Output.antiquotation @{binding noindent} (Scan.succeed ()) (K (K "\\noindent")) #>
- Thy_Output.antiquotation @{binding smallskip} (Scan.succeed ()) (K (K "\\smallskip")) #>
- Thy_Output.antiquotation @{binding medskip} (Scan.succeed ()) (K (K "\\medskip")) #>
- Thy_Output.antiquotation @{binding bigskip} (Scan.succeed ()) (K (K "\\bigskip")));
+ (Thy_Output.antiquotation \<^binding>\<open>noindent\<close> (Scan.succeed ()) (K (K "\\noindent")) #>
+ Thy_Output.antiquotation \<^binding>\<open>smallskip\<close> (Scan.succeed ()) (K (K "\\smallskip")) #>
+ Thy_Output.antiquotation \<^binding>\<open>medskip\<close> (Scan.succeed ()) (K (K "\\medskip")) #>
+ Thy_Output.antiquotation \<^binding>\<open>bigskip\<close> (Scan.succeed ()) (K (K "\\bigskip")));
(* control style *)
@@ -50,9 +50,9 @@
val _ =
Theory.setup
- (control_antiquotation @{binding footnote} "\\footnote{" "}" #>
- control_antiquotation @{binding emph} "\\emph{" "}" #>
- control_antiquotation @{binding bold} "\\textbf{" "}");
+ (control_antiquotation \<^binding>\<open>footnote\<close> "\\footnote{" "}" #>
+ control_antiquotation \<^binding>\<open>emph\<close> "\\emph{" "}" #>
+ control_antiquotation \<^binding>\<open>bold\<close> "\\textbf{" "}");
end;
@@ -72,8 +72,8 @@
val _ =
Theory.setup
- (text_antiquotation @{binding text} #>
- text_antiquotation @{binding cartouche});
+ (text_antiquotation \<^binding>\<open>text\<close> #>
+ text_antiquotation \<^binding>\<open>cartouche\<close>);
end;
@@ -82,7 +82,7 @@
val _ =
Theory.setup
- (Thy_Output.antiquotation @{binding theory_text} (Scan.lift Args.text_input)
+ (Thy_Output.antiquotation \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
(fn {context = ctxt, ...} => fn source =>
let
val _ =
@@ -122,8 +122,8 @@
in
val _ = Theory.setup
- (goal_state @{binding goals} true #>
- goal_state @{binding subgoals} false);
+ (goal_state \<^binding>\<open>goals\<close> true #>
+ goal_state \<^binding>\<open>subgoals\<close> false);
end;
@@ -131,7 +131,7 @@
(* embedded lemma *)
val _ = Theory.setup
- (Thy_Output.antiquotation @{binding lemma}
+ (Thy_Output.antiquotation \<^binding>\<open>lemma\<close>
(Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
(fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
@@ -156,7 +156,7 @@
val _ =
Theory.setup
- (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.text_input)
+ (Thy_Output.antiquotation \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
(fn {context = ctxt, ...} => fn source =>
(Context_Position.report ctxt (Input.pos_of source)
(Markup.language_verbatim (Input.is_delimited source));
@@ -178,18 +178,18 @@
in
val _ = Theory.setup
- (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>
- ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #>
- ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #>
- ml_text @{binding ML_structure}
+ (ml_text \<^binding>\<open>ML\<close> (ml_enclose "fn _ => (" ");") #>
+ ml_text \<^binding>\<open>ML_op\<close> (ml_enclose "fn _ => (op " ");") #>
+ ml_text \<^binding>\<open>ML_type\<close> (ml_enclose "val _ = NONE : (" ") option;") #>
+ ml_text \<^binding>\<open>ML_structure\<close>
(ml_enclose "functor XXX() = struct structure XX = " " end;") #>
- ml_text @{binding ML_functor} (* FIXME formal treatment of functor name (!?) *)
+ ml_text \<^binding>\<open>ML_functor\<close> (* FIXME formal treatment of functor name (!?) *)
(fn source =>
ML_Lex.read ("ML_Env.check_functor " ^
ML_Syntax.print_string (Input.source_content source))) #>
- ml_text @{binding ML_text} (K []));
+ ml_text \<^binding>\<open>ML_text\<close> (K []));
end;
@@ -197,7 +197,7 @@
(* URLs *)
val _ = Theory.setup
- (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.embedded))
+ (Thy_Output.antiquotation \<^binding>\<open>url\<close> (Scan.lift (Parse.position Parse.embedded))
(fn {context = ctxt, ...} => fn (name, pos) =>
(Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
enclose "\\url{" "}" name)));
@@ -206,7 +206,7 @@
(* doc entries *)
val _ = Theory.setup
- (Thy_Output.antiquotation @{binding doc} (Scan.lift (Parse.position Parse.embedded))
+ (Thy_Output.antiquotation \<^binding>\<open>doc\<close> (Scan.lift (Parse.position Parse.embedded))
(fn {context = ctxt, ...} => fn (name, pos) =>
(Context_Position.report ctxt pos (Markup.doc name);
Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name])));
@@ -220,11 +220,11 @@
val _ =
Theory.setup
- (entity_antiquotation @{binding command} Outer_Syntax.check_command
+ (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command
(enclose "\\isacommand{" "}" o Output.output) #>
- entity_antiquotation @{binding method} Method.check_name
+ entity_antiquotation \<^binding>\<open>method\<close> Method.check_name
(enclose "\\isa{" "}" o Output.output) #>
- entity_antiquotation @{binding attribute} Attrib.check_name
+ entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name
(enclose "\\isa{" "}" o Output.output));
end;
--- a/src/Pure/Thy/term_style.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Thy/term_style.ML Wed Dec 06 18:59:33 2017 +0100
@@ -82,10 +82,10 @@
| sub_term t = t;
val _ = Theory.setup
- (setup @{binding lhs} (style_lhs_rhs fst) #>
- setup @{binding rhs} (style_lhs_rhs snd) #>
- setup @{binding prem} style_prem #>
- setup @{binding concl} (Scan.succeed (K Logic.strip_imp_concl)) #>
- setup @{binding sub} (Scan.succeed (K sub_term)));
+ (setup \<^binding>\<open>lhs\<close> (style_lhs_rhs fst) #>
+ setup \<^binding>\<open>rhs\<close> (style_lhs_rhs snd) #>
+ setup \<^binding>\<open>prem\<close> style_prem #>
+ setup \<^binding>\<open>concl\<close> (Scan.succeed (K Logic.strip_imp_concl)) #>
+ setup \<^binding>\<open>sub\<close> (Scan.succeed (K sub_term)));
end;
--- a/src/Pure/Thy/thy_output.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Dec 06 18:59:33 2017 +0100
@@ -487,7 +487,7 @@
(* present commands *)
- val document_tags = space_explode "," (Options.default_string @{system_option document_tags});
+ val document_tags = space_explode "," (Options.default_string \<^system_option>\<open>document_tags\<close>);
fun present_command tr span st st' =
Toplevel.setmp_thread_position tr (present_span keywords document_tags span st st');
@@ -511,23 +511,23 @@
(* options *)
val _ = Theory.setup
- (add_option @{binding show_types} (Config.put show_types o boolean) #>
- add_option @{binding show_sorts} (Config.put show_sorts o boolean) #>
- add_option @{binding show_structs} (Config.put show_structs o boolean) #>
- add_option @{binding show_question_marks} (Config.put show_question_marks o boolean) #>
- add_option @{binding show_abbrevs} (Config.put show_abbrevs o boolean) #>
- add_option @{binding names_long} (Config.put Name_Space.names_long o boolean) #>
- add_option @{binding names_short} (Config.put Name_Space.names_short o boolean) #>
- add_option @{binding names_unique} (Config.put Name_Space.names_unique o boolean) #>
- add_option @{binding eta_contract} (Config.put Syntax_Trans.eta_contract o boolean) #>
- add_option @{binding display} (Config.put display o boolean) #>
- add_option @{binding break} (Config.put break o boolean) #>
- add_option @{binding quotes} (Config.put quotes o boolean) #>
- add_option @{binding mode} (add_wrapper o Print_Mode.with_modes o single) #>
- add_option @{binding margin} (Config.put margin o integer) #>
- add_option @{binding indent} (Config.put indent o integer) #>
- add_option @{binding source} (Config.put source o boolean) #>
- add_option @{binding goals_limit} (Config.put Goal_Display.goals_limit o integer));
+ (add_option \<^binding>\<open>show_types\<close> (Config.put show_types o boolean) #>
+ add_option \<^binding>\<open>show_sorts\<close> (Config.put show_sorts o boolean) #>
+ add_option \<^binding>\<open>show_structs\<close> (Config.put show_structs o boolean) #>
+ add_option \<^binding>\<open>show_question_marks\<close> (Config.put show_question_marks o boolean) #>
+ add_option \<^binding>\<open>show_abbrevs\<close> (Config.put show_abbrevs o boolean) #>
+ add_option \<^binding>\<open>names_long\<close> (Config.put Name_Space.names_long o boolean) #>
+ add_option \<^binding>\<open>names_short\<close> (Config.put Name_Space.names_short o boolean) #>
+ add_option \<^binding>\<open>names_unique\<close> (Config.put Name_Space.names_unique o boolean) #>
+ add_option \<^binding>\<open>eta_contract\<close> (Config.put Syntax_Trans.eta_contract o boolean) #>
+ add_option \<^binding>\<open>display\<close> (Config.put display o boolean) #>
+ add_option \<^binding>\<open>break\<close> (Config.put break o boolean) #>
+ add_option \<^binding>\<open>quotes\<close> (Config.put quotes o boolean) #>
+ add_option \<^binding>\<open>mode\<close> (add_wrapper o Print_Mode.with_modes o single) #>
+ add_option \<^binding>\<open>margin\<close> (Config.put margin o integer) #>
+ add_option \<^binding>\<open>indent\<close> (Config.put indent o integer) #>
+ add_option \<^binding>\<open>source\<close> (Config.put source o boolean) #>
+ add_option \<^binding>\<open>goals_limit\<close> (Config.put Goal_Display.goals_limit o integer));
(* basic pretty printing *)
@@ -647,20 +647,20 @@
in
val _ = Theory.setup
- (basic_entities_style @{binding thm} (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
- basic_entity @{binding prop} (Term_Style.parse -- Args.prop) pretty_term_style #>
- basic_entity @{binding term} (Term_Style.parse -- Args.term) pretty_term_style #>
- basic_entity @{binding term_type} (Term_Style.parse -- Args.term) pretty_term_typ #>
- basic_entity @{binding typeof} (Term_Style.parse -- Args.term) pretty_term_typeof #>
- basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
- basic_entity @{binding abbrev} (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
- basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
- basic_entity @{binding locale} (Scan.lift (Parse.position Args.name)) pretty_locale #>
- basic_entity @{binding class} (Scan.lift Args.embedded_inner_syntax) pretty_class #>
- basic_entity @{binding type} (Scan.lift Args.embedded) pretty_type #>
- basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
- basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
- basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);
+ (basic_entities_style \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
+ basic_entity \<^binding>\<open>prop\<close> (Term_Style.parse -- Args.prop) pretty_term_style #>
+ basic_entity \<^binding>\<open>term\<close> (Term_Style.parse -- Args.term) pretty_term_style #>
+ basic_entity \<^binding>\<open>term_type\<close> (Term_Style.parse -- Args.term) pretty_term_typ #>
+ basic_entity \<^binding>\<open>typeof\<close> (Term_Style.parse -- Args.term) pretty_term_typeof #>
+ basic_entity \<^binding>\<open>const\<close> (Args.const {proper = true, strict = false}) pretty_const #>
+ basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
+ basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #>
+ basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.name)) pretty_locale #>
+ basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #>
+ basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded) pretty_type #>
+ basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #>
+ basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
+ basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.name)) pretty_theory);
end;
--- a/src/Pure/Tools/bibtex.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Tools/bibtex.ML Wed Dec 06 18:59:33 2017 +0100
@@ -12,12 +12,12 @@
structure Bibtex: BIBTEX =
struct
-val cite_macro = Attrib.setup_config_string @{binding cite_macro} (K "cite");
+val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "cite");
val _ =
Theory.setup
- (Thy_Output.add_option @{binding cite_macro} (Config.put cite_macro) #>
- Thy_Output.antiquotation @{binding cite}
+ (Thy_Output.add_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
+ Thy_Output.antiquotation \<^binding>\<open>cite\<close>
(Scan.lift
(Scan.option (Parse.verbatim || Parse.cartouche) --
Parse.and_list1 (Parse.position Args.name)))
--- a/src/Pure/Tools/find_theorems.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Tools/find_theorems.ML Wed Dec 06 18:59:33 2017 +0100
@@ -190,7 +190,7 @@
val goal' = Thm.transfer thy' goal;
fun limited_etac thm i =
- Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o
+ Seq.take (Options.default_int \<^system_option>\<open>find_theorems_tactic_limit\<close>) o
eresolve_tac ctxt' [thm] i;
fun try_thm thm =
if Thm.no_prems thm then resolve_tac ctxt' [thm] 1 goal'
@@ -414,7 +414,7 @@
else raw_matches;
val len = length matches;
- val lim = the_default (Options.default_int @{system_option find_theorems_limit}) opt_limit;
+ val lim = the_default (Options.default_int \<^system_option>\<open>find_theorems_limit\<close>) opt_limit;
in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
val find =
--- a/src/Pure/Tools/jedit.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Tools/jedit.ML Wed Dec 06 18:59:33 2017 +0100
@@ -75,7 +75,7 @@
val _ =
Theory.setup
- (Thy_Output.antiquotation @{binding action} (Scan.lift (Parse.position Parse.embedded))
+ (Thy_Output.antiquotation \<^binding>\<open>action\<close> (Scan.lift (Parse.position Parse.embedded))
(fn {context = ctxt, ...} => fn (name, pos) =>
(if Context_Position.is_reported ctxt pos then ignore (check_action (name, pos)) else ();
Thy_Output.verbatim_text ctxt name)));
--- a/src/Pure/Tools/named_theorems.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Tools/named_theorems.ML Wed Dec 06 18:59:33 2017 +0100
@@ -97,7 +97,7 @@
(* ML antiquotation *)
val _ = Theory.setup
- (ML_Antiquotation.inline @{binding named_theorems}
+ (ML_Antiquotation.inline \<^binding>\<open>named_theorems\<close>
(Args.context -- Scan.lift (Parse.position Args.embedded) >>
(fn (ctxt, name) => ML_Syntax.print_string (check ctxt name))));
--- a/src/Pure/Tools/plugin.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Tools/plugin.ML Wed Dec 06 18:59:33 2017 +0100
@@ -40,7 +40,7 @@
#1 o Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt));
val _ = Theory.setup
- (ML_Antiquotation.inline @{binding plugin}
+ (ML_Antiquotation.inline \<^binding>\<open>plugin\<close>
(Args.context -- Scan.lift (Parse.position Args.embedded)
>> (ML_Syntax.print_string o uncurry check)));
--- a/src/Pure/Tools/rail.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Tools/rail.ML Wed Dec 06 18:59:33 2017 +0100
@@ -374,7 +374,7 @@
in Latex.environment "railoutput" (implode (map output_rule rules)) end;
val _ = Theory.setup
- (Thy_Output.antiquotation @{binding rail} (Scan.lift Args.text_input)
+ (Thy_Output.antiquotation \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
(fn {state, context, ...} => output_rules state o read context));
end;
--- a/src/Pure/Tools/rule_insts.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Tools/rule_insts.ML Wed Dec 06 18:59:33 2017 +0100
@@ -182,7 +182,7 @@
-- Parse.for_fixes;
val _ = Theory.setup
- (Attrib.setup @{binding "where"}
+ (Attrib.setup \<^binding>\<open>where\<close>
(Scan.lift named_insts >> (fn args =>
Thm.rule_attribute [] (fn context => uncurry (where_rule (Context.proof_of context)) args)))
"named instantiation of theorem");
@@ -202,7 +202,7 @@
in
val _ = Theory.setup
- (Attrib.setup @{binding "of"}
+ (Attrib.setup \<^binding>\<open>of\<close>
(Scan.lift (insts -- Parse.for_fixes) >> (fn args =>
Thm.rule_attribute [] (fn context => uncurry (of_rule (Context.proof_of context)) args)))
"positional instantiation of theorem");
@@ -320,22 +320,22 @@
(*warning: rule_tac etc. refer to dynamic subgoal context!*)
val _ = Theory.setup
- (Method.setup @{binding rule_tac} (method res_inst_tac resolve_tac)
+ (Method.setup \<^binding>\<open>rule_tac\<close> (method res_inst_tac resolve_tac)
"apply rule (dynamic instantiation)" #>
- Method.setup @{binding erule_tac} (method eres_inst_tac eresolve_tac)
+ Method.setup \<^binding>\<open>erule_tac\<close> (method eres_inst_tac eresolve_tac)
"apply rule in elimination manner (dynamic instantiation)" #>
- Method.setup @{binding drule_tac} (method dres_inst_tac dresolve_tac)
+ Method.setup \<^binding>\<open>drule_tac\<close> (method dres_inst_tac dresolve_tac)
"apply rule in destruct manner (dynamic instantiation)" #>
- Method.setup @{binding frule_tac} (method forw_inst_tac forward_tac)
+ Method.setup \<^binding>\<open>frule_tac\<close> (method forw_inst_tac forward_tac)
"apply rule in forward manner (dynamic instantiation)" #>
- Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
+ Method.setup \<^binding>\<open>cut_tac\<close> (method cut_inst_tac (K cut_rules_tac))
"cut rule (dynamic instantiation)" #>
- Method.setup @{binding subgoal_tac}
+ Method.setup \<^binding>\<open>subgoal_tac\<close>
(Args.goal_spec -- Scan.lift (Scan.repeat1 Args.embedded_inner_syntax -- Parse.for_fixes) >>
(fn (quant, (props, fixes)) => fn ctxt =>
SIMPLE_METHOD'' quant (EVERY' (map (fn prop => subgoal_tac ctxt prop fixes) props))))
"insert subgoal (dynamic instantiation)" #>
- Method.setup @{binding thin_tac}
+ Method.setup \<^binding>\<open>thin_tac\<close>
(Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
(fn (quant, (prop, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop fixes)))
"remove premise (dynamic instantiation)");
--- a/src/Pure/Tools/simplifier_trace.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML Wed Dec 06 18:59:33 2017 +0100
@@ -438,10 +438,10 @@
(fn (((interactive, mode), depth), memory) => config mode interactive depth memory)
val _ = Theory.setup
- (Attrib.setup @{binding simp_break}
+ (Attrib.setup \<^binding>\<open>simp_break\<close>
(Scan.repeat Args.term_pattern >> breakpoint)
"declaration of a simplifier breakpoint" #>
- Attrib.setup @{binding simp_trace_new} (Scan.lift config_parser)
+ Attrib.setup \<^binding>\<open>simp_trace_new\<close> (Scan.lift config_parser)
"simplifier trace configuration")
end
--- a/src/Pure/simplifier.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/simplifier.ML Wed Dec 06 18:59:33 2017 +0100
@@ -112,7 +112,7 @@
val the_simproc = Name_Space.get o get_simprocs;
val _ = Theory.setup
- (ML_Antiquotation.value @{binding simproc}
+ (ML_Antiquotation.value \<^binding>\<open>simproc\<close>
(Args.context -- Scan.lift (Parse.position Args.embedded)
>> (fn (ctxt, name) =>
"Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
@@ -319,13 +319,13 @@
(* setup attributes *)
val _ = Theory.setup
- (Attrib.setup @{binding simp} (Attrib.add_del simp_add simp_del)
+ (Attrib.setup \<^binding>\<open>simp\<close> (Attrib.add_del simp_add simp_del)
"declaration of Simplifier rewrite rule" #>
- Attrib.setup @{binding cong} (Attrib.add_del cong_add cong_del)
+ Attrib.setup \<^binding>\<open>cong\<close> (Attrib.add_del cong_add cong_del)
"declaration of Simplifier congruence rule" #>
- Attrib.setup @{binding simproc} simproc_att
+ Attrib.setup \<^binding>\<open>simproc\<close> simproc_att
"declaration of simplification procedures" #>
- Attrib.setup @{binding simplified} simplified "simplified rule");
+ Attrib.setup \<^binding>\<open>simplified\<close> simplified "simplified rule");
@@ -368,12 +368,12 @@
(** setup **)
fun method_setup more_mods =
- Method.setup @{binding simp}
+ Method.setup \<^binding>\<open>simp\<close>
(simp_method more_mods (fn ctxt => fn tac => fn facts =>
HEADGOAL (Method.insert_tac ctxt facts THEN'
(CHANGED_PROP oo tac) ctxt)))
"simplification" #>
- Method.setup @{binding simp_all}
+ Method.setup \<^binding>\<open>simp_all\<close>
(simp_method more_mods (fn ctxt => fn tac => fn facts =>
ALLGOALS (Method.insert_tac ctxt facts) THEN
(CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt))