--- a/NEWS Mon Apr 06 16:30:44 2015 +0200
+++ b/NEWS Mon Apr 06 17:06:48 2015 +0200
@@ -407,6 +407,10 @@
* Goal.prove_multi is superseded by the fully general Goal.prove_common,
which also allows to specify a fork priority.
+* Antiquotation @{command_spec "COMMAND"} is superseded by
+@{command_keyword COMMAND} (usually without quotes and with PIDE
+markup). Minor INCOMPATIBILITY.
+
*** System ***
--- a/src/HOL/Decision_Procs/approximation.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML Mon Apr 06 17:06:48 2015 +0200
@@ -244,7 +244,7 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
val _ =
- Outer_Syntax.command @{command_spec "approximate"} "print approximation of term"
+ Outer_Syntax.command @{command_keyword approximate} "print approximation of term"
(opt_modes -- Parse.term
>> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Mon Apr 06 17:06:48 2015 +0200
@@ -261,7 +261,7 @@
end
val _ =
- Outer_Syntax.command @{command_spec "domain"} "define recursive domains (HOLCF)"
+ Outer_Syntax.command @{command_keyword domain} "define recursive domains (HOLCF)"
(domains_decl >> (Toplevel.theory o mk_domain))
end
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Apr 06 17:06:48 2015 +0200
@@ -755,7 +755,7 @@
in
val _ =
- Outer_Syntax.command @{command_spec "domain_isomorphism"} "define domain isomorphisms (HOLCF)"
+ Outer_Syntax.command @{command_keyword domain_isomorphism} "define domain isomorphisms (HOLCF)"
(parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd))
end
--- a/src/HOL/HOLCF/Tools/cpodef.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Mon Apr 06 17:06:48 2015 +0200
@@ -332,12 +332,12 @@
((t, args, mx), A, morphs)
val _ =
- Outer_Syntax.command @{command_spec "pcpodef"}
+ Outer_Syntax.command @{command_keyword pcpodef}
"HOLCF type definition (requires admissibility proof)"
(typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof true))
val _ =
- Outer_Syntax.command @{command_spec "cpodef"}
+ Outer_Syntax.command @{command_keyword cpodef}
"HOLCF type definition (requires admissibility proof)"
(typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof false))
--- a/src/HOL/HOLCF/Tools/domaindef.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Mon Apr 06 17:06:48 2015 +0200
@@ -209,7 +209,7 @@
domaindef_cmd ((t, args, mx), A, morphs)
val _ =
- Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations"
+ Outer_Syntax.command @{command_keyword domaindef} "HOLCF definition of domains from deflations"
(domaindef_decl >> (Toplevel.theory o mk_domaindef))
end
--- a/src/HOL/HOLCF/Tools/fixrec.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Mon Apr 06 17:06:48 2015 +0200
@@ -399,7 +399,7 @@
in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! @{keyword "|"})) end
val _ =
- Outer_Syntax.local_theory @{command_spec "fixrec"} "define recursive functions (HOLCF)"
+ Outer_Syntax.local_theory @{command_keyword fixrec} "define recursive functions (HOLCF)"
(Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
>> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
--- a/src/HOL/Import/import_data.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Import/import_data.ML Mon Apr 06 17:06:48 2015 +0200
@@ -117,13 +117,13 @@
"declare a type_definition theorem as a map for an imported type with abs and rep")
val _ =
- Outer_Syntax.command @{command_spec "import_type_map"}
+ Outer_Syntax.command @{command_keyword import_type_map}
"map external type name to existing Isabelle/HOL type name"
((Parse.name --| @{keyword ":"}) -- Parse.type_const >>
(fn (ty_name1, ty_name2) => Toplevel.theory (add_typ_map_cmd ty_name1 ty_name2)))
val _ =
- Outer_Syntax.command @{command_spec "import_const_map"}
+ Outer_Syntax.command @{command_keyword import_const_map}
"map external const name to existing Isabelle/HOL const name"
((Parse.name --| @{keyword ":"}) -- Parse.const >>
(fn (cname1, cname2) => Toplevel.theory (add_const_map_cmd cname1 cname2)))
--- a/src/HOL/Import/import_rule.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Import/import_rule.ML Mon Apr 06 17:06:48 2015 +0200
@@ -444,7 +444,7 @@
fun process_file path thy =
(thy, init_state) |> File.fold_lines process_line path |> fst
-val _ = Outer_Syntax.command @{command_spec "import_file"}
+val _ = Outer_Syntax.command @{command_keyword import_file}
"import a recorded proof file"
(Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
--- a/src/HOL/Library/Old_SMT/old_smt_config.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_config.ML Mon Apr 06 17:06:48 2015 +0200
@@ -246,7 +246,7 @@
end
val _ =
- Outer_Syntax.command @{command_spec "old_smt_status"}
+ Outer_Syntax.command @{command_keyword old_smt_status}
"show the available SMT solvers, the currently selected SMT solver, \
\and the values of SMT configuration options"
(Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
--- a/src/HOL/Library/bnf_axiomatization.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML Mon Apr 06 17:06:48 2015 +0200
@@ -118,7 +118,7 @@
parse_witTs -- Parse.opt_mixfix -- parse_map_rel_bindings;
val _ =
- Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration"
+ Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration"
(parse_bnf_axiomatization >>
(fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb)) =>
bnf_axiomatization_cmd plugins bsTs b mx mapb relb witTs #> snd));
--- a/src/HOL/Library/code_test.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Library/code_test.ML Mon Apr 06 17:06:48 2015 +0200
@@ -567,7 +567,7 @@
val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
val _ =
- Outer_Syntax.command @{command_spec "test_code"}
+ Outer_Syntax.command @{command_keyword test_code}
"compile test cases to target languages, execute them and report results"
(test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
--- a/src/HOL/Library/refute.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Library/refute.ML Mon Apr 06 17:06:48 2015 +0200
@@ -2965,7 +2965,7 @@
(* 'refute' command *)
val _ =
- Outer_Syntax.command @{command_spec "refute"}
+ Outer_Syntax.command @{command_keyword refute}
"try to find a model that refutes a given subgoal"
(scan_parms -- Scan.optional Parse.nat 1 >>
(fn (parms, i) =>
@@ -2980,7 +2980,7 @@
(* 'refute_params' command *)
val _ =
- Outer_Syntax.command @{command_spec "refute_params"}
+ Outer_Syntax.command @{command_keyword refute_params}
"show/store default parameters for the 'refute' command"
(scan_parms >> (fn parms =>
Toplevel.theory (fn thy =>
--- a/src/HOL/Library/simps_case_conv.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Library/simps_case_conv.ML Mon Apr 06 17:06:48 2015 +0200
@@ -219,7 +219,7 @@
end
val _ =
- Outer_Syntax.local_theory @{command_spec "case_of_simps"}
+ Outer_Syntax.local_theory @{command_keyword case_of_simps}
"turn a list of equations into a case expression"
(Parse_Spec.opt_thm_name ":" -- Parse.xthms1 >> case_of_simps_cmd)
@@ -227,7 +227,7 @@
Parse.xthms1 --| @{keyword ")"}
val _ =
- Outer_Syntax.local_theory @{command_spec "simps_of_case"}
+ Outer_Syntax.local_theory @{command_keyword simps_of_case}
"perform case split on rule"
(Parse_Spec.opt_thm_name ":" -- Parse.xthm --
Scan.optional parse_splits [] >> simps_of_case_cmd)
--- a/src/HOL/Nominal/nominal_atoms.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Mon Apr 06 17:06:48 2015 +0200
@@ -1018,7 +1018,7 @@
(* syntax und parsing *)
val _ =
- Outer_Syntax.command @{command_spec "atom_decl"} "declare new kinds of atoms"
+ Outer_Syntax.command @{command_keyword atom_decl} "declare new kinds of atoms"
(Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
end;
--- a/src/HOL/Nominal/nominal_datatype.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Apr 06 17:06:48 2015 +0200
@@ -2074,7 +2074,7 @@
val nominal_datatype_cmd = gen_nominal_datatype Old_Datatype.read_specs;
val _ =
- Outer_Syntax.command @{command_spec "nominal_datatype"} "define nominal datatypes"
+ Outer_Syntax.command @{command_keyword nominal_datatype} "define nominal datatypes"
(Parse.and_list1 Old_Datatype.spec_cmd >>
(Toplevel.theory o nominal_datatype_cmd Old_Datatype_Aux.default_config));
--- a/src/HOL/Nominal/nominal_inductive.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon Apr 06 17:06:48 2015 +0200
@@ -671,14 +671,14 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive}
"prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
(Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
(@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
prove_strong_ind name avoids));
val _ =
- Outer_Syntax.local_theory @{command_spec "equivariance"}
+ Outer_Syntax.local_theory @{command_keyword equivariance}
"prove equivariance for inductive predicate involving nominal datatypes"
(Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
(fn (name, atoms) => prove_eqvt name atoms));
--- a/src/HOL/Nominal/nominal_inductive2.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Apr 06 17:06:48 2015 +0200
@@ -483,7 +483,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive2"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive2}
"prove strong induction theorem for inductive predicate involving nominal datatypes"
(Parse.xname --
Scan.option (@{keyword "("} |-- Parse.!!! (Parse.name --| @{keyword ")"})) --
--- a/src/HOL/Nominal/nominal_primrec.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Mon Apr 06 17:06:48 2015 +0200
@@ -403,7 +403,7 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "nominal_primrec"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword nominal_primrec}
"define primitive recursive functions on nominal datatypes"
(options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
>> (fn ((((invs, fctxt), fixes), params), specs) =>
--- a/src/HOL/Orderings.thy Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Orderings.thy Mon Apr 06 17:06:48 2015 +0200
@@ -439,7 +439,7 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "print_orders"}
+ Outer_Syntax.command @{command_keyword print_orders}
"print order structures available to transitivity reasoner"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (print_structures o Toplevel.context_of)));
--- a/src/HOL/SMT_Examples/boogie.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/SMT_Examples/boogie.ML Mon Apr 06 17:06:48 2015 +0200
@@ -266,7 +266,7 @@
(* Isar command *)
val _ =
- Outer_Syntax.command @{command_spec "boogie_file"}
+ Outer_Syntax.command @{command_keyword boogie_file}
"prove verification condition from .b2i file"
(Resources.provide_parse_files "boogie_file" >> (fn files =>
Toplevel.theory (fn thy =>
--- a/src/HOL/SPARK/Tools/spark_commands.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Mon Apr 06 17:06:48 2015 +0200
@@ -92,13 +92,13 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "spark_open_vcg"}
+ Outer_Syntax.command @{command_keyword spark_open_vcg}
"open a new SPARK environment and load a SPARK-generated .vcg file"
(Resources.provide_parse_files "spark_open_vcg" -- Parse.parname
>> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
val _ =
- Outer_Syntax.command @{command_spec "spark_open"}
+ Outer_Syntax.command @{command_keyword spark_open}
"open a new SPARK environment and load a SPARK-generated .siv file"
(Resources.provide_parse_files "spark_open" -- Parse.parname
>> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
@@ -107,13 +107,13 @@
(Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);
val _ =
- Outer_Syntax.command @{command_spec "spark_proof_functions"}
+ Outer_Syntax.command @{command_keyword spark_proof_functions}
"associate SPARK proof functions with terms"
(Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >>
(Toplevel.theory o fold add_proof_fun_cmd));
val _ =
- Outer_Syntax.command @{command_spec "spark_types"}
+ Outer_Syntax.command @{command_keyword spark_types}
"associate SPARK types with types"
(Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
Scan.optional (Args.parens (Parse.list1
@@ -121,12 +121,12 @@
(Toplevel.theory o fold add_spark_type_cmd));
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "spark_vc"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword spark_vc}
"enter into proof mode for a specific verification condition"
(Parse.name >> prove_vc);
val _ =
- Outer_Syntax.command @{command_spec "spark_status"}
+ Outer_Syntax.command @{command_keyword spark_status}
"show the name and state of all loaded verification conditions"
(Scan.optional
(Args.parens
@@ -136,7 +136,7 @@
Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args)))
val _ =
- Outer_Syntax.command @{command_spec "spark_end"}
+ Outer_Syntax.command @{command_keyword spark_end}
"close the current SPARK environment"
(Scan.optional (@{keyword "("} |-- Parse.!!!
(Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >>
--- a/src/HOL/Statespace/state_space.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Statespace/state_space.ML Mon Apr 06 17:06:48 2015 +0200
@@ -650,7 +650,7 @@
(plus1_unless comp parent --
Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
val _ =
- Outer_Syntax.command @{command_spec "statespace"} "define state-space as locale context"
+ Outer_Syntax.command @{command_keyword statespace} "define state-space as locale context"
(statespace_decl >> (fn ((args, name), (parents, comps)) =>
Toplevel.theory (define_statespace args name parents comps)));
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Apr 06 17:06:48 2015 +0200
@@ -912,7 +912,7 @@
in TPTP_Data.map (cons ((prob_name, result))) thy' end
val _ =
- Outer_Syntax.command @{command_spec "import_tptp"} "import TPTP problem"
+ Outer_Syntax.command @{command_keyword import_tptp} "import TPTP problem"
(Parse.path >> (fn name =>
Toplevel.theory (fn thy =>
let val path = Path.explode name
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Mon Apr 06 17:06:48 2015 +0200
@@ -1854,7 +1854,7 @@
(*This has been disabled since it requires a hook to be specified to use "import_thm"
val _ =
- Outer_Syntax.command @{command_spec "import_leo2_proof"} "import TPTP proof"
+ Outer_Syntax.command @{command_keyword import_leo2_proof} "import TPTP proof"
(Parse.path >> (fn name =>
Toplevel.theory (fn thy =>
let val path = Path.explode name
--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Apr 06 17:06:48 2015 +0200
@@ -1615,12 +1615,12 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "print_bnfs"}
+ Outer_Syntax.command @{command_keyword print_bnfs}
"print all bounded natural functors"
(Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "bnf"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword bnf}
"register a type as a bounded natural functor"
(parse_opt_binding_colon -- Parse.typ --|
(Parse.reserved "map" -- @{keyword ":"}) -- Parse.term --
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Apr 06 17:06:48 2015 +0200
@@ -2019,7 +2019,7 @@
val fake_T = qsoty (unfreeze_fp X);
val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop);
fun register_hint () =
- "\nUse the " ^ quote (#1 @{command_spec "bnf"}) ^ " command to register " ^
+ "\nUse the " ^ quote (#1 @{command_keyword bnf}) ^ " command to register " ^
quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
\it";
in
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Apr 06 17:06:48 2015 +0200
@@ -2555,7 +2555,7 @@
end;
val _ =
- Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes"
+ Outer_Syntax.local_theory @{command_keyword codatatype} "define coinductive datatypes"
(parse_co_datatype_cmd Greatest_FP construct_gfp);
val _ = Theory.setup (fp_antiquote_setup @{binding codatatype});
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Apr 06 17:06:48 2015 +0200
@@ -112,8 +112,8 @@
fun unexpected_corec_call ctxt eqns t =
error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
fun use_primcorecursive () =
- error ("\"auto\" failed (try " ^ quote (#1 @{command_spec "primcorecursive"}) ^ " instead of " ^
- quote (#1 @{command_spec "primcorec"}) ^ ")");
+ error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^
+ quote (#1 @{command_keyword primcorec}) ^ ")");
datatype corec_option =
Plugins_Option of Proof.context -> Plugin_Name.filter |
@@ -1551,13 +1551,13 @@
val where_alt_props_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
((Parse.prop >> pair Attrib.empty_binding) -- Scan.option (Parse.reserved "of" |-- Parse.const)));
-val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"}
+val _ = Outer_Syntax.local_theory_to_proof @{command_keyword primcorecursive}
"define primitive corecursive functions"
((Scan.optional (@{keyword "("} |--
Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
(Parse.fixes -- where_alt_props_of_parser) >> uncurry add_primcorecursive_cmd);
-val _ = Outer_Syntax.local_theory @{command_spec "primcorec"}
+val _ = Outer_Syntax.local_theory @{command_keyword primcorec}
"define primitive corecursive functions"
((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
--| @{keyword ")"}) []) --
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Apr 06 17:06:48 2015 +0200
@@ -1842,7 +1842,7 @@
end;
val _ =
- Outer_Syntax.local_theory @{command_spec "datatype"} "define inductive datatypes"
+ Outer_Syntax.local_theory @{command_keyword datatype} "define inductive datatypes"
(parse_co_datatype_cmd Least_FP construct_lfp);
val _ = Theory.setup (fp_antiquote_setup @{binding datatype});
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Apr 06 17:06:48 2015 +0200
@@ -539,7 +539,7 @@
BNF_LFP_Rec_Sugar.add_primrec_simple;
val _ =
- Outer_Syntax.local_theory @{command_spec "datatype_compat"}
+ Outer_Syntax.local_theory @{command_keyword datatype_compat}
"register datatypes as old-style datatypes and derive old-style properties"
(Scan.repeat1 Parse.type_const >> datatype_compat_cmd);
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Apr 06 17:06:48 2015 +0200
@@ -669,7 +669,7 @@
|| Parse.reserved "nonexhaustive" >> K Nonexhaustive_Option
|| Parse.reserved "transfer" >> K Transfer_Option);
-val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
+val _ = Outer_Syntax.local_theory @{command_keyword primrec}
"define primitive recursive functions"
((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
--| @{keyword ")"}) []) --
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Mon Apr 06 17:06:48 2015 +0200
@@ -630,7 +630,7 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "print_case_translations"}
+ Outer_Syntax.command @{command_keyword print_case_translations}
"print registered case combinators and constructors"
(Scan.succeed (Toplevel.keep (print_case_translations o Toplevel.context_of)))
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Apr 06 17:06:48 2015 +0200
@@ -1143,7 +1143,7 @@
val parse_sel_default_eqs = Scan.optional (@{keyword "where"} |-- Parse.enum1 "|" Parse.prop) [];
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword free_constructors}
"register an existing freely generated type's constructors"
(parse_ctr_options -- Parse.binding --| @{keyword "for"} -- parse_ctr_specs
-- parse_sel_default_eqs
--- a/src/HOL/Tools/Function/fun.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Function/fun.ML Mon Apr 06 17:06:48 2015 +0200
@@ -172,7 +172,7 @@
val _ =
- Outer_Syntax.local_theory' @{command_spec "fun"}
+ Outer_Syntax.local_theory' @{command_keyword fun}
"define general recursive functions (short version)"
(function_parser fun_config
>> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
--- a/src/HOL/Tools/Function/fun_cases.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML Mon Apr 06 17:06:48 2015 +0200
@@ -54,7 +54,7 @@
val fun_cases_cmd = gen_fun_cases Attrib.check_src Syntax.read_prop;
val _ =
- Outer_Syntax.local_theory @{command_spec "fun_cases"}
+ Outer_Syntax.local_theory @{command_keyword fun_cases}
"create simplified instances of elimination rules for function equations"
(Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
--- a/src/HOL/Tools/Function/function.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Function/function.ML Mon Apr 06 17:06:48 2015 +0200
@@ -286,13 +286,13 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory_to_proof' @{command_spec "function"}
+ Outer_Syntax.local_theory_to_proof' @{command_keyword function}
"define general recursive functions"
(function_parser default_config
>> (fn ((config, fixes), statements) => function_cmd fixes statements config))
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword termination}
"prove termination of a recursive function"
(Scan.option Parse.term >> termination_cmd)
--- a/src/HOL/Tools/Function/partial_function.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Mon Apr 06 17:06:48 2015 +0200
@@ -309,7 +309,7 @@
val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
val _ =
- Outer_Syntax.local_theory @{command_spec "partial_function"} "define partial function"
+ Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
>> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
--- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Apr 06 17:06:48 2015 +0200
@@ -700,7 +700,7 @@
--| @{keyword "is"} -- Parse.term --
Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword lift_definition}
"definition for constants over the quotient type"
(liftdef_parser >> lift_def_cmd_with_err_handling)
--- a/src/HOL/Tools/Lifting/lifting_info.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Mon Apr 06 17:06:48 2015 +0200
@@ -533,11 +533,11 @@
(* outer syntax commands *)
val _ =
- Outer_Syntax.command @{command_spec "print_quot_maps"} "print quotient map functions"
+ Outer_Syntax.command @{command_keyword print_quot_maps} "print quotient map functions"
(Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of)))
val _ =
- Outer_Syntax.command @{command_spec "print_quotients"} "print quotients"
+ Outer_Syntax.command @{command_keyword print_quotients} "print quotients"
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
end
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Apr 06 17:06:48 2015 +0200
@@ -787,7 +787,7 @@
end
val _ =
- Outer_Syntax.local_theory @{command_spec "setup_lifting"}
+ Outer_Syntax.local_theory @{command_keyword setup_lifting}
"setup lifting infrastructure"
(Parse.xthm -- Scan.option Parse.xthm
-- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >>
@@ -998,7 +998,7 @@
val _ =
- Outer_Syntax.local_theory @{command_spec "lifting_forget"}
+ Outer_Syntax.local_theory @{command_keyword lifting_forget}
"unsetup Lifting and Transfer for the given lifting bundle"
(Parse.position Parse.xname >> (lifting_forget_cmd))
@@ -1027,7 +1027,7 @@
update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy
val _ =
- Outer_Syntax.local_theory @{command_spec "lifting_update"}
+ Outer_Syntax.local_theory @{command_keyword lifting_update}
"add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
(Parse.position Parse.xname >> lifting_update_cmd)
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Mon Apr 06 17:06:48 2015 +0200
@@ -374,7 +374,7 @@
|> sort_strings |> cat_lines)))))
val _ =
- Outer_Syntax.command @{command_spec "nitpick"}
+ Outer_Syntax.command @{command_keyword nitpick}
"try to find a counterexample for a given subgoal using Nitpick"
(parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
Toplevel.unknown_proof o
@@ -383,7 +383,7 @@
(Toplevel.proof_of state)))))
val _ =
- Outer_Syntax.command @{command_spec "nitpick_params"}
+ Outer_Syntax.command @{command_keyword nitpick_params}
"set and display the default parameters for Nitpick"
(parse_params #>> nitpick_params_trans)
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Mon Apr 06 17:06:48 2015 +0200
@@ -788,7 +788,7 @@
>> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
val _ =
- Outer_Syntax.command @{command_spec "old_datatype"} "define old-style inductive datatypes"
+ Outer_Syntax.command @{command_keyword old_datatype} "define old-style inductive datatypes"
(Parse.and_list1 spec_cmd
>> (Toplevel.theory o (snd oo add_datatype_cmd Old_Datatype_Aux.default_config)));
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Mon Apr 06 17:06:48 2015 +0200
@@ -680,7 +680,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.command @{command_spec "old_rep_datatype"}
+ Outer_Syntax.command @{command_keyword old_rep_datatype}
"register existing types as old-style datatypes"
(Scan.repeat1 Parse.term >> (fn ts =>
Toplevel.theory_to_proof (rep_datatype_cmd Old_Datatype_Aux.default_config (K I) ts)));
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Apr 06 17:06:48 2015 +0200
@@ -1033,7 +1033,7 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
val _ =
- Outer_Syntax.command @{command_spec "values_prolog"}
+ Outer_Syntax.command @{command_keyword values_prolog}
"enumerate and print comprehensions"
(opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
>> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t)))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon Apr 06 17:06:48 2015 +0200
@@ -278,12 +278,12 @@
(* code_pred command and values command *)
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "code_pred"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword code_pred}
"prove equations for predicate specified by intro/elim rules"
(opt_expected_modes -- opt_modes -- scan_options -- Parse.term >> code_pred_cmd)
val _ =
- Outer_Syntax.command @{command_spec "values"}
+ Outer_Syntax.command @{command_keyword values}
"enumerate and print comprehensions"
(opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
>> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Mon Apr 06 17:06:48 2015 +0200
@@ -67,7 +67,7 @@
Syntax.read_term
val _ =
- Outer_Syntax.command @{command_spec "quickcheck_generator"}
+ Outer_Syntax.command @{command_keyword quickcheck_generator}
"define quickcheck generators for abstract types"
((Parse.type_const --
Scan.option (Args.$$$ "predicate" |-- @{keyword ":"} |-- Parse.term)) --
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Apr 06 17:06:48 2015 +0200
@@ -111,7 +111,7 @@
end
val _ =
- Outer_Syntax.command @{command_spec "find_unused_assms"}
+ Outer_Syntax.command @{command_keyword find_unused_assms}
"find theorems with (potentially) superfluous assumptions"
(Scan.option Parse.name >> (fn name =>
Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name)))
--- a/src/HOL/Tools/Quotient/quotient_def.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon Apr 06 17:06:48 2015 +0200
@@ -213,7 +213,7 @@
Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "quotient_definition"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword quotient_definition}
"definition for constants over the quotient type"
(quotdef_parser >> quotient_def_cmd)
--- a/src/HOL/Tools/Quotient/quotient_info.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Mon Apr 06 17:06:48 2015 +0200
@@ -229,15 +229,15 @@
(* outer syntax commands *)
val _ =
- Outer_Syntax.command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
+ Outer_Syntax.command @{command_keyword print_quotmapsQ3} "print quotient map functions"
(Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
val _ =
- Outer_Syntax.command @{command_spec "print_quotientsQ3"} "print quotients"
+ Outer_Syntax.command @{command_keyword print_quotientsQ3} "print quotients"
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
val _ =
- Outer_Syntax.command @{command_spec "print_quotconsts"} "print quotient constants"
+ Outer_Syntax.command @{command_keyword print_quotconsts} "print quotient constants"
(Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
end;
--- a/src/HOL/Tools/Quotient/quotient_type.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Mon Apr 06 17:06:48 2015 +0200
@@ -342,7 +342,7 @@
-- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm)
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword quotient_type}
"quotient type definitions (require equivalence proofs)"
(quotspec_parser >> quotient_type_cmd)
--- a/src/HOL/Tools/SMT/smt_config.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML Mon Apr 06 17:06:48 2015 +0200
@@ -257,7 +257,7 @@
end
val _ =
- Outer_Syntax.command @{command_spec "smt_status"}
+ Outer_Syntax.command @{command_keyword smt_status}
"show the available SMT solvers, the currently selected SMT solver, \
\and the values of SMT configuration options"
(Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Apr 06 17:06:48 2015 +0200
@@ -387,12 +387,12 @@
no_fact_override
val _ =
- Outer_Syntax.command @{command_spec "sledgehammer"}
+ Outer_Syntax.command @{command_keyword sledgehammer}
"search for first-order proof using automatic theorem provers"
((Scan.optional Parse.name runN -- parse_params
-- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
val _ =
- Outer_Syntax.command @{command_spec "sledgehammer_params"}
+ Outer_Syntax.command @{command_keyword sledgehammer_params}
"set and display the default parameters for Sledgehammer"
(parse_params #>> sledgehammer_params_trans)
--- a/src/HOL/Tools/choice_specification.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML Mon Apr 06 17:06:48 2015 +0200
@@ -198,7 +198,7 @@
val opt_overloaded = Parse.opt_keyword "overloaded"
val _ =
- Outer_Syntax.command @{command_spec "specification"} "define constants by specification"
+ Outer_Syntax.command @{command_keyword specification} "define constants by specification"
(@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
>> (fn (cos, alt_props) => Toplevel.theory_to_proof (process_spec cos alt_props)))
--- a/src/HOL/Tools/functor.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/functor.ML Mon Apr 06 17:06:48 2015 +0200
@@ -273,7 +273,7 @@
val functor_cmd = gen_functor Syntax.read_term;
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "functor"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword functor}
"register operations managing the functorial structure of a type"
(Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
>> (fn (prfx, t) => functor_cmd prfx t));
--- a/src/HOL/Tools/inductive.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/inductive.ML Mon Apr 06 17:06:48 2015 +0200
@@ -1171,25 +1171,25 @@
val ind_decl = gen_ind_decl add_ind_def;
val _ =
- Outer_Syntax.local_theory @{command_spec "inductive"} "define inductive predicates"
+ Outer_Syntax.local_theory @{command_keyword inductive} "define inductive predicates"
(ind_decl false);
val _ =
- Outer_Syntax.local_theory @{command_spec "coinductive"} "define coinductive predicates"
+ Outer_Syntax.local_theory @{command_keyword coinductive} "define coinductive predicates"
(ind_decl true);
val _ =
- Outer_Syntax.local_theory @{command_spec "inductive_cases"}
+ Outer_Syntax.local_theory @{command_keyword inductive_cases}
"create simplified instances of elimination rules"
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
val _ =
- Outer_Syntax.local_theory @{command_spec "inductive_simps"}
+ Outer_Syntax.local_theory @{command_keyword inductive_simps}
"create simplification rules for inductive predicates"
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
val _ =
- Outer_Syntax.command @{command_spec "print_inductives"}
+ Outer_Syntax.command @{command_keyword print_inductives}
"print (co)inductive definitions and monotonicity rules"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (print_inductives b o Toplevel.context_of)));
--- a/src/HOL/Tools/inductive_set.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML Mon Apr 06 17:06:48 2015 +0200
@@ -568,11 +568,11 @@
val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
val _ =
- Outer_Syntax.local_theory @{command_spec "inductive_set"} "define inductive sets"
+ Outer_Syntax.local_theory @{command_keyword inductive_set} "define inductive sets"
(ind_set_decl false);
val _ =
- Outer_Syntax.local_theory @{command_spec "coinductive_set"} "define coinductive sets"
+ Outer_Syntax.local_theory @{command_keyword coinductive_set} "define coinductive sets"
(ind_set_decl true);
end;
--- a/src/HOL/Tools/recdef.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/recdef.ML Mon Apr 06 17:06:48 2015 +0200
@@ -298,7 +298,7 @@
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
val _ =
- Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (obsolete TFL)"
+ Outer_Syntax.command @{command_keyword recdef} "define general recursive functions (obsolete TFL)"
(recdef_decl >> Toplevel.theory);
@@ -309,12 +309,12 @@
>> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
val _ =
- Outer_Syntax.command @{command_spec "defer_recdef"}
+ Outer_Syntax.command @{command_keyword defer_recdef}
"defer general recursive functions (obsolete TFL)"
(defer_recdef_decl >> Toplevel.theory);
val _ =
- Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"}
+ Outer_Syntax.local_theory_to_proof' @{command_keyword recdef_tc}
"recommence proof of termination condition (obsolete TFL)"
((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
--- a/src/HOL/Tools/record.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/record.ML Mon Apr 06 17:06:48 2015 +0200
@@ -2329,7 +2329,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.command @{command_spec "record"} "define extensible record"
+ Outer_Syntax.command @{command_keyword record} "define extensible record"
(Parse.type_args_constrained -- Parse.binding --
(@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
Scan.repeat1 Parse.const_binding)
--- a/src/HOL/Tools/try0.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/try0.ML Mon Apr 06 17:06:48 2015 +0200
@@ -177,7 +177,7 @@
|| Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x;
val _ =
- Outer_Syntax.command @{command_spec "try0"} "try a combination of proof methods"
+ Outer_Syntax.command @{command_keyword try0} "try a combination of proof methods"
(Scan.optional parse_attrs ([], [], [], []) #>> try0_trans);
fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
--- a/src/HOL/Tools/typedef.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/typedef.ML Mon Apr 06 17:06:48 2015 +0200
@@ -281,7 +281,7 @@
(** outer syntax **)
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "typedef"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword typedef}
"HOL type definition (requires non-emptiness proof)"
(Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
(@{keyword "="} |-- Parse.term) --
--- a/src/HOL/Tools/value.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/value.ML Mon Apr 06 17:06:48 2015 +0200
@@ -70,7 +70,7 @@
Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
val _ =
- Outer_Syntax.command @{command_spec "value"} "evaluate and print term"
+ Outer_Syntax.command @{command_keyword value} "evaluate and print term"
(opt_evaluator -- opt_modes -- Parse.term
>> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
--- a/src/HOL/ex/Cartouche_Examples.thy Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy Mon Apr 06 17:06:48 2015 +0200
@@ -40,7 +40,7 @@
subsection \<open>Outer syntax: cartouche within command syntax\<close>
ML \<open>
- Outer_Syntax.command @{command_spec "cartouche"} ""
+ Outer_Syntax.command @{command_keyword cartouche} ""
(Parse.cartouche >> (fn s =>
Toplevel.imperative (fn () => writeln s)))
\<close>
@@ -116,7 +116,7 @@
subsubsection \<open>Term cartouche and regular quotes\<close>
ML \<open>
- Outer_Syntax.command @{command_spec "term_cartouche"} ""
+ Outer_Syntax.command @{command_keyword term_cartouche} ""
(Parse.inner_syntax Parse.cartouche >> (fn s =>
Toplevel.keep (fn state =>
let
@@ -178,7 +178,7 @@
ML \<open>
Outer_Syntax.command
- @{command_spec "text_cartouche"} ""
+ @{command_keyword text_cartouche} ""
(Parse.opt_target -- Parse.input Parse.cartouche >> Thy_Output.document_command)
\<close>
--- a/src/HOL/ex/Commands.thy Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/ex/Commands.thy Mon Apr 06 17:06:48 2015 +0200
@@ -15,7 +15,7 @@
subsection \<open>Diagnostic command: no state change\<close>
ML \<open>
- Outer_Syntax.command @{command_spec "print_test"} "print term test"
+ Outer_Syntax.command @{command_keyword print_test} "print term test"
(Parse.term >> (fn s => Toplevel.keep (fn st =>
let
val ctxt = Toplevel.context_of st;
@@ -30,7 +30,7 @@
subsection \<open>Old-style global theory declaration\<close>
ML \<open>
- Outer_Syntax.command @{command_spec "global_test"} "test constant declaration"
+ Outer_Syntax.command @{command_keyword global_test} "test constant declaration"
(Parse.binding >> (fn b => Toplevel.theory (fn thy =>
let
val thy' = Sign.add_consts [(b, @{typ 'a}, NoSyn)] thy;
@@ -45,7 +45,7 @@
subsection \<open>Local theory specification\<close>
ML \<open>
- Outer_Syntax.local_theory @{command_spec "local_test"} "test local definition"
+ Outer_Syntax.local_theory @{command_keyword local_test} "test local definition"
(Parse.binding -- (@{keyword "="} |-- Parse.term) >> (fn (b, s) => fn lthy =>
let
val t = Syntax.read_term lthy s;
--- a/src/Provers/classical.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Provers/classical.ML Mon Apr 06 17:06:48 2015 +0200
@@ -974,7 +974,7 @@
(** outer syntax **)
val _ =
- Outer_Syntax.command @{command_spec "print_claset"} "print context of Classical Reasoner"
+ Outer_Syntax.command @{command_keyword print_claset} "print context of Classical Reasoner"
(Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
end;
--- a/src/Pure/Isar/calculation.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Pure/Isar/calculation.ML Mon Apr 06 17:06:48 2015 +0200
@@ -211,25 +211,25 @@
Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
val _ =
- Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
+ Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
(calc_args >> (Toplevel.proofs' o also_cmd));
val _ =
- Outer_Syntax.command @{command_spec "finally"}
+ Outer_Syntax.command @{command_keyword finally}
"combine calculation and current facts, exhibit result"
(calc_args >> (Toplevel.proofs' o finally_cmd));
val _ =
- Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
+ Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts"
(Scan.succeed (Toplevel.proof' moreover));
val _ =
- Outer_Syntax.command @{command_spec "ultimately"}
+ Outer_Syntax.command @{command_keyword ultimately}
"augment calculation by current facts, exhibit result"
(Scan.succeed (Toplevel.proof' ultimately));
val _ =
- Outer_Syntax.command @{command_spec "print_trans_rules"} "print transitivity rules"
+ Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
(Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
end;
--- a/src/Pure/Isar/isar_syn.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Apr 06 17:06:48 2015 +0200
@@ -12,7 +12,7 @@
(* sorts *)
val _ =
- Outer_Syntax.local_theory @{command_spec "default_sort"}
+ Outer_Syntax.local_theory @{command_keyword default_sort}
"declare default sort for explicit type variables"
(Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
@@ -20,18 +20,18 @@
(* types *)
val _ =
- Outer_Syntax.local_theory @{command_spec "typedecl"} "type declaration"
+ Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
(Parse.type_args -- Parse.binding -- Parse.opt_mixfix
>> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
val _ =
- Outer_Syntax.local_theory @{command_spec "type_synonym"} "declare type abbreviation"
+ Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
(Parse.type_args -- Parse.binding --
(@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
>> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
val _ =
- Outer_Syntax.command @{command_spec "nonterminal"}
+ Outer_Syntax.command @{command_keyword nonterminal}
"declare syntactic type constructors (grammar nonterminal symbols)"
(Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
@@ -39,11 +39,11 @@
(* consts and syntax *)
val _ =
- Outer_Syntax.command @{command_spec "judgment"} "declare object-logic judgment"
+ Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment"
(Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
val _ =
- Outer_Syntax.command @{command_spec "consts"} "declare constants"
+ Outer_Syntax.command @{command_keyword consts} "declare constants"
(Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
val mode_spec =
@@ -54,12 +54,12 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default;
val _ =
- Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses"
+ Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses"
(opt_mode -- Scan.repeat1 Parse.const_decl
>> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
val _ =
- Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses"
+ Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses"
(opt_mode -- Scan.repeat1 Parse.const_decl
>> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
@@ -81,11 +81,11 @@
>> (fn (left, (arr, right)) => arr (left, right));
val _ =
- Outer_Syntax.command @{command_spec "translations"} "add syntax translation rules"
+ Outer_Syntax.command @{command_keyword translations} "add syntax translation rules"
(Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
val _ =
- Outer_Syntax.command @{command_spec "no_translations"} "delete syntax translation rules"
+ Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules"
(Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
@@ -98,7 +98,7 @@
@{keyword "overloaded"} >> K (false, true)) --| @{keyword ")"})) (false, false);
val _ =
- Outer_Syntax.command @{command_spec "defs"} "define constants"
+ Outer_Syntax.command @{command_keyword defs} "define constants"
(opt_unchecked_overloaded --
Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
>> (Toplevel.theory o Isar_Cmd.add_defs));
@@ -107,34 +107,34 @@
(* constant definitions and abbreviations *)
val _ =
- Outer_Syntax.local_theory' @{command_spec "definition"} "constant definition"
+ Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
(Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
val _ =
- Outer_Syntax.local_theory' @{command_spec "abbreviation"} "constant abbreviation"
+ Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
(opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
>> (fn (mode, args) => Specification.abbreviation_cmd mode args));
val _ =
- Outer_Syntax.local_theory @{command_spec "type_notation"}
+ Outer_Syntax.local_theory @{command_keyword type_notation}
"add concrete syntax for type constructors"
(opt_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_spec "no_type_notation"}
+ Outer_Syntax.local_theory @{command_keyword no_type_notation}
"delete concrete syntax for type constructors"
(opt_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_spec "notation"}
+ Outer_Syntax.local_theory @{command_keyword notation}
"add concrete syntax for constants / fixed variables"
(opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
>> (fn (mode, args) => Specification.notation_cmd true mode args));
val _ =
- Outer_Syntax.local_theory @{command_spec "no_notation"}
+ Outer_Syntax.local_theory @{command_keyword no_notation}
"delete concrete syntax for constants / fixed variables"
(opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
>> (fn (mode, args) => Specification.notation_cmd false mode args));
@@ -143,7 +143,7 @@
(* constant specifications *)
val _ =
- Outer_Syntax.command @{command_spec "axiomatization"} "axiomatic constant specification"
+ Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
(Scan.optional Parse.fixes [] --
Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
>> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
@@ -156,14 +156,14 @@
>> (fn (facts, fixes) => #2 oo Specification.theorems_cmd kind facts fixes);
val _ =
- Outer_Syntax.local_theory' @{command_spec "theorems"} "define theorems"
+ Outer_Syntax.local_theory' @{command_keyword theorems} "define theorems"
(theorems Thm.theoremK);
val _ =
- Outer_Syntax.local_theory' @{command_spec "lemmas"} "define lemmas" (theorems Thm.lemmaK);
+ Outer_Syntax.local_theory' @{command_keyword lemmas} "define lemmas" (theorems Thm.lemmaK);
val _ =
- Outer_Syntax.local_theory' @{command_spec "declare"} "declare theorems"
+ Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
(Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
>> (fn (facts, fixes) =>
#2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
@@ -183,19 +183,19 @@
in
val _ =
- hide_names @{command_spec "hide_class"} "classes" Sign.hide_class Parse.class
+ hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class
Proof_Context.read_class;
val _ =
- hide_names @{command_spec "hide_type"} "types" Sign.hide_type Parse.type_const
+ hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const
((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
val _ =
- hide_names @{command_spec "hide_const"} "constants" Sign.hide_const Parse.const
+ hide_names @{command_keyword hide_const} "constants" Sign.hide_const Parse.const
((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
val _ =
- hide_names @{command_spec "hide_fact"} "facts" Global_Theory.hide_fact
+ hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
(Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
end;
@@ -204,7 +204,7 @@
(* use ML text *)
val _ =
- Outer_Syntax.command @{command_spec "SML_file"} "read and evaluate Standard ML file"
+ Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file"
(Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
let
val ([{lines, pos, ...}], thy') = files thy;
@@ -216,7 +216,7 @@
end)));
val _ =
- Outer_Syntax.command @{command_spec "SML_export"} "evaluate SML within Isabelle/ML environment"
+ Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
(Parse.ML_source >> (fn source =>
let val flags = {SML = true, exchange = true, redirect = false, verbose = true} in
Toplevel.theory
@@ -224,7 +224,7 @@
end));
val _ =
- Outer_Syntax.command @{command_spec "SML_import"} "evaluate Isabelle/ML within SML environment"
+ Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment"
(Parse.ML_source >> (fn source =>
let val flags = {SML = false, exchange = true, redirect = false, verbose = true} in
Toplevel.generic_theory
@@ -233,7 +233,7 @@
end));
val _ =
- Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
+ Outer_Syntax.command @{command_keyword ML} "ML text within theory or local theory"
(Parse.ML_source >> (fn source =>
Toplevel.generic_theory
(ML_Context.exec (fn () =>
@@ -241,7 +241,7 @@
Local_Theory.propagate_ml_env)));
val _ =
- Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
+ Outer_Syntax.command @{command_keyword ML_prf} "ML text within proof"
(Parse.ML_source >> (fn source =>
Toplevel.proof (Proof.map_context (Context.proof_map
(ML_Context.exec (fn () =>
@@ -249,45 +249,45 @@
Proof.propagate_ml_env)));
val _ =
- Outer_Syntax.command @{command_spec "ML_val"} "diagnostic ML text"
+ Outer_Syntax.command @{command_keyword ML_val} "diagnostic ML text"
(Parse.ML_source >> Isar_Cmd.ml_diag true);
val _ =
- Outer_Syntax.command @{command_spec "ML_command"} "diagnostic ML text (silent)"
+ Outer_Syntax.command @{command_keyword ML_command} "diagnostic ML text (silent)"
(Parse.ML_source >> Isar_Cmd.ml_diag false);
val _ =
- Outer_Syntax.command @{command_spec "setup"} "ML setup for global theory"
+ Outer_Syntax.command @{command_keyword setup} "ML setup for global theory"
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup));
val _ =
- Outer_Syntax.local_theory @{command_spec "local_setup"} "ML setup for local theory"
+ Outer_Syntax.local_theory @{command_keyword local_setup} "ML setup for local theory"
(Parse.ML_source >> Isar_Cmd.local_setup);
val _ =
- Outer_Syntax.local_theory @{command_spec "attribute_setup"} "define attribute in ML"
+ Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML"
(Parse.position Parse.name --
Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
>> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
val _ =
- Outer_Syntax.local_theory @{command_spec "method_setup"} "define proof method in ML"
+ Outer_Syntax.local_theory @{command_keyword method_setup} "define proof method in ML"
(Parse.position Parse.name --
Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
>> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
val _ =
- Outer_Syntax.local_theory @{command_spec "declaration"} "generic ML declaration"
+ Outer_Syntax.local_theory @{command_keyword declaration} "generic ML declaration"
(Parse.opt_keyword "pervasive" -- Parse.ML_source
>> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
val _ =
- Outer_Syntax.local_theory @{command_spec "syntax_declaration"} "generic ML syntax declaration"
+ Outer_Syntax.local_theory @{command_keyword syntax_declaration} "generic ML syntax declaration"
(Parse.opt_keyword "pervasive" -- Parse.ML_source
>> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
val _ =
- Outer_Syntax.local_theory @{command_spec "simproc_setup"} "define simproc in ML"
+ Outer_Syntax.local_theory @{command_keyword simproc_setup} "define simproc in ML"
(Parse.position Parse.name --
(@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) --
Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
@@ -297,27 +297,27 @@
(* translation functions *)
val _ =
- Outer_Syntax.command @{command_spec "parse_ast_translation"}
+ Outer_Syntax.command @{command_keyword parse_ast_translation}
"install parse ast translation functions"
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
val _ =
- Outer_Syntax.command @{command_spec "parse_translation"}
+ Outer_Syntax.command @{command_keyword parse_translation}
"install parse translation functions"
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation));
val _ =
- Outer_Syntax.command @{command_spec "print_translation"}
+ Outer_Syntax.command @{command_keyword print_translation}
"install print translation functions"
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation));
val _ =
- Outer_Syntax.command @{command_spec "typed_print_translation"}
+ Outer_Syntax.command @{command_keyword typed_print_translation}
"install typed print translation functions"
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
val _ =
- Outer_Syntax.command @{command_spec "print_ast_translation"}
+ Outer_Syntax.command @{command_keyword print_ast_translation}
"install print ast translation functions"
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
@@ -325,7 +325,7 @@
(* oracles *)
val _ =
- Outer_Syntax.command @{command_spec "oracle"} "declare oracle"
+ Outer_Syntax.command @{command_keyword oracle} "declare oracle"
(Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
(fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
@@ -333,22 +333,22 @@
(* bundled declarations *)
val _ =
- Outer_Syntax.local_theory @{command_spec "bundle"} "define bundle of declarations"
+ Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
((Parse.binding --| @{keyword "="}) -- Parse.xthms1 -- Parse.for_fixes
>> (uncurry Bundle.bundle_cmd));
val _ =
- Outer_Syntax.command @{command_spec "include"}
+ Outer_Syntax.command @{command_keyword include}
"include declarations from bundle in proof body"
(Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
val _ =
- Outer_Syntax.command @{command_spec "including"}
+ Outer_Syntax.command @{command_keyword including}
"include declarations from bundle in goal refinement"
(Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
val _ =
- Outer_Syntax.command @{command_spec "print_bundles"}
+ Outer_Syntax.command @{command_keyword print_bundles}
"print bundles of declarations"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
@@ -357,7 +357,7 @@
(* local theories *)
val _ =
- Outer_Syntax.command @{command_spec "context"} "begin local theory context"
+ Outer_Syntax.command @{command_keyword context} "begin local theory context"
((Parse.position Parse.xname >> (fn name =>
Toplevel.begin_local_theory true (Named_Target.begin name)) ||
Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
@@ -373,7 +373,7 @@
Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
val _ =
- Outer_Syntax.command @{command_spec "locale"} "define named specification context"
+ Outer_Syntax.command @{command_keyword locale} "define named specification context"
(Parse.binding --
Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
>> (fn ((name, (expr, elems)), begin) =>
@@ -381,7 +381,7 @@
(Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
val _ =
- Outer_Syntax.command @{command_spec "experiment"} "open private specification context"
+ Outer_Syntax.command @{command_keyword experiment} "open private specification context"
(Scan.repeat Parse_Spec.context_element --| Parse.begin
>> (fn elems =>
Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
@@ -392,7 +392,7 @@
(Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
val _ =
- Outer_Syntax.command @{command_spec "sublocale"}
+ Outer_Syntax.command @{command_keyword sublocale}
"prove sublocale relation between a locale and a locale expression"
((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
interpretation_args false >> (fn (loc, (expr, equations)) =>
@@ -401,13 +401,13 @@
Toplevel.local_theory_to_proof NONE NONE (Expression.sublocale_cmd expr equations)));
val _ =
- Outer_Syntax.command @{command_spec "interpretation"}
+ Outer_Syntax.command @{command_keyword interpretation}
"prove interpretation of locale expression in local theory"
(interpretation_args true >> (fn (expr, equations) =>
Toplevel.local_theory_to_proof NONE NONE (Expression.interpretation_cmd expr equations)));
val _ =
- Outer_Syntax.command @{command_spec "interpret"}
+ Outer_Syntax.command @{command_keyword interpret}
"prove interpretation of locale expression in proof context"
(interpretation_args true >> (fn (expr, equations) =>
Toplevel.proof' (Expression.interpret_cmd expr equations)));
@@ -421,23 +421,23 @@
Scan.repeat1 Parse_Spec.context_element >> pair [];
val _ =
- Outer_Syntax.command @{command_spec "class"} "define type class"
+ Outer_Syntax.command @{command_keyword class} "define type class"
(Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
>> (fn ((name, (supclasses, elems)), begin) =>
Toplevel.begin_local_theory begin
(Class_Declaration.class_cmd name supclasses elems #> snd)));
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "subclass"} "prove a subclass relation"
+ Outer_Syntax.local_theory_to_proof @{command_keyword subclass} "prove a subclass relation"
(Parse.class >> Class_Declaration.subclass_cmd);
val _ =
- Outer_Syntax.command @{command_spec "instantiation"} "instantiate and prove type arity"
+ Outer_Syntax.command @{command_keyword instantiation} "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_spec "instance"} "prove type arity or subclass relation"
+ Outer_Syntax.command @{command_keyword instance} "prove type arity or subclass relation"
((Parse.class --
((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
@@ -447,7 +447,7 @@
(* arbitrary overloading *)
val _ =
- Outer_Syntax.command @{command_spec "overloading"} "overloaded definitions"
+ Outer_Syntax.command @{command_keyword overloading} "overloaded definitions"
(Scan.repeat1 (Parse.name --| (@{keyword "\<equiv>"} || @{keyword "=="}) -- Parse.term --
Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
>> Parse.triple1) --| Parse.begin
@@ -457,7 +457,7 @@
(* code generation *)
val _ =
- Outer_Syntax.command @{command_spec "code_datatype"}
+ Outer_Syntax.command @{command_keyword code_datatype}
"define set of code datatype constructors"
(Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
@@ -478,32 +478,32 @@
((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
kind NONE (K I) a includes elems concl)));
-val _ = theorem @{command_spec "theorem"} false Thm.theoremK;
-val _ = theorem @{command_spec "lemma"} false Thm.lemmaK;
-val _ = theorem @{command_spec "corollary"} false Thm.corollaryK;
-val _ = theorem @{command_spec "schematic_theorem"} true Thm.theoremK;
-val _ = theorem @{command_spec "schematic_lemma"} true Thm.lemmaK;
-val _ = theorem @{command_spec "schematic_corollary"} true Thm.corollaryK;
+val _ = theorem @{command_keyword theorem} false Thm.theoremK;
+val _ = theorem @{command_keyword lemma} false Thm.lemmaK;
+val _ = theorem @{command_keyword corollary} false Thm.corollaryK;
+val _ = theorem @{command_keyword schematic_theorem} true Thm.theoremK;
+val _ = theorem @{command_keyword schematic_lemma} true Thm.lemmaK;
+val _ = theorem @{command_keyword schematic_corollary} true Thm.corollaryK;
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "notepad"} "begin proof context"
+ Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
(Parse.begin >> K Proof.begin_notepad);
val _ =
- Outer_Syntax.command @{command_spec "have"} "state local goal"
+ Outer_Syntax.command @{command_keyword have} "state local goal"
(Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.have));
val _ =
- Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\""
+ Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
(Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.hence));
val _ =
- Outer_Syntax.command @{command_spec "show"}
+ Outer_Syntax.command @{command_keyword show}
"state local goal, solving current obligation"
(Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.show));
val _ =
- Outer_Syntax.command @{command_spec "thus"} "old-style alias of \"then show\""
+ Outer_Syntax.command @{command_keyword thus} "old-style alias of \"then show\""
(Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.thus));
@@ -512,46 +512,46 @@
val facts = Parse.and_list1 Parse.xthms1;
val _ =
- Outer_Syntax.command @{command_spec "then"} "forward chaining"
+ Outer_Syntax.command @{command_keyword then} "forward chaining"
(Scan.succeed (Toplevel.proof Proof.chain));
val _ =
- Outer_Syntax.command @{command_spec "from"} "forward chaining from given facts"
+ Outer_Syntax.command @{command_keyword from} "forward chaining from given facts"
(facts >> (Toplevel.proof o Proof.from_thmss_cmd));
val _ =
- Outer_Syntax.command @{command_spec "with"} "forward chaining from given and current facts"
+ Outer_Syntax.command @{command_keyword with} "forward chaining from given and current facts"
(facts >> (Toplevel.proof o Proof.with_thmss_cmd));
val _ =
- Outer_Syntax.command @{command_spec "note"} "define facts"
+ Outer_Syntax.command @{command_keyword note} "define facts"
(Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
val _ =
- Outer_Syntax.command @{command_spec "using"} "augment goal facts"
+ Outer_Syntax.command @{command_keyword using} "augment goal facts"
(facts >> (Toplevel.proof o Proof.using_cmd));
val _ =
- Outer_Syntax.command @{command_spec "unfolding"} "unfold definitions in goal and facts"
+ Outer_Syntax.command @{command_keyword unfolding} "unfold definitions in goal and facts"
(facts >> (Toplevel.proof o Proof.unfolding_cmd));
(* proof context *)
val _ =
- Outer_Syntax.command @{command_spec "fix"} "fix local variables (Skolem constants)"
+ Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)"
(Parse.fixes >> (Toplevel.proof o Proof.fix_cmd));
val _ =
- Outer_Syntax.command @{command_spec "assume"} "assume propositions"
+ Outer_Syntax.command @{command_keyword assume} "assume propositions"
(Parse_Spec.statement >> (Toplevel.proof o Proof.assume_cmd));
val _ =
- Outer_Syntax.command @{command_spec "presume"} "assume propositions, to be established later"
+ Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later"
(Parse_Spec.statement >> (Toplevel.proof o Proof.presume_cmd));
val _ =
- Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)"
+ Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
(Parse.and_list1
(Parse_Spec.opt_thm_name ":" --
((Parse.binding -- Parse.opt_mixfix) --
@@ -559,26 +559,26 @@
>> (Toplevel.proof o Proof.def_cmd));
val _ =
- Outer_Syntax.command @{command_spec "obtain"} "generalized elimination"
+ Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
(Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
>> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
val _ =
- Outer_Syntax.command @{command_spec "guess"} "wild guessing (unstructured)"
+ Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
(Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd));
val _ =
- Outer_Syntax.command @{command_spec "let"} "bind text variables"
+ Outer_Syntax.command @{command_keyword let} "bind text variables"
(Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
>> (Toplevel.proof o Proof.let_bind_cmd));
val _ =
- Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables"
+ Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables"
(opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
>> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
val _ =
- Outer_Syntax.command @{command_spec "case"} "invoke local context"
+ Outer_Syntax.command @{command_keyword case} "invoke local context"
((@{keyword "("} |--
Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
--| @{keyword ")"}) ||
@@ -589,74 +589,74 @@
(* proof structure *)
val _ =
- Outer_Syntax.command @{command_spec "{"} "begin explicit proof block"
+ Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block"
(Scan.succeed (Toplevel.proof Proof.begin_block));
val _ =
- Outer_Syntax.command @{command_spec "}"} "end explicit proof block"
+ Outer_Syntax.command @{command_keyword "}"} "end explicit proof block"
(Scan.succeed (Toplevel.proof Proof.end_block));
val _ =
- Outer_Syntax.command @{command_spec "next"} "enter next proof block"
+ Outer_Syntax.command @{command_keyword next} "enter next proof block"
(Scan.succeed (Toplevel.proof Proof.next_block));
(* end proof *)
val _ =
- Outer_Syntax.command @{command_spec "qed"} "conclude proof"
+ Outer_Syntax.command @{command_keyword qed} "conclude proof"
(Scan.option Method.parse >> (fn m =>
(Option.map Method.report m;
Isar_Cmd.qed m)));
val _ =
- Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
+ Outer_Syntax.command @{command_keyword by} "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_spec ".."} "default proof"
+ Outer_Syntax.command @{command_keyword ".."} "default proof"
(Scan.succeed Isar_Cmd.default_proof);
val _ =
- Outer_Syntax.command @{command_spec "."} "immediate proof"
+ Outer_Syntax.command @{command_keyword "."} "immediate proof"
(Scan.succeed Isar_Cmd.immediate_proof);
val _ =
- Outer_Syntax.command @{command_spec "done"} "done proof"
+ Outer_Syntax.command @{command_keyword done} "done proof"
(Scan.succeed Isar_Cmd.done_proof);
val _ =
- Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)"
+ Outer_Syntax.command @{command_keyword sorry} "skip proof (quick-and-dirty mode only!)"
(Scan.succeed Isar_Cmd.skip_proof);
val _ =
- Outer_Syntax.command @{command_spec "oops"} "forget proof"
+ Outer_Syntax.command @{command_keyword oops} "forget proof"
(Scan.succeed (Toplevel.forget_proof true));
(* proof steps *)
val _ =
- Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
+ Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state"
(Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
val _ =
- Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
+ Outer_Syntax.command @{command_keyword prefer} "shuffle internal proof state"
(Parse.nat >> (Toplevel.proof o Proof.prefer));
val _ =
- Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
+ Outer_Syntax.command @{command_keyword apply} "initial refinement step (unstructured)"
(Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_results m))));
val _ =
- Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
+ Outer_Syntax.command @{command_keyword apply_end} "terminal refinement step (unstructured)"
(Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end_results m))));
val _ =
- Outer_Syntax.command @{command_spec "proof"} "backward proof step"
+ Outer_Syntax.command @{command_keyword proof} "backward proof step"
(Scan.option Method.parse >> (fn m =>
(Option.map Method.report m;
Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
@@ -669,7 +669,7 @@
Output.report [Markup.markup Markup.bad "Explicit backtracking"];
val _ =
- Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command"
+ Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
(Scan.succeed
(Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
Toplevel.skip_proof (fn h => (report_back (); h))));
@@ -682,194 +682,194 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
val _ =
- Outer_Syntax.command @{command_spec "help"}
+ Outer_Syntax.command @{command_keyword help}
"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_spec "print_commands"} "print outer syntax commands"
+ Outer_Syntax.command @{command_keyword print_commands} "print outer syntax commands"
(Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_options"} "print configuration options"
+ Outer_Syntax.command @{command_keyword print_options} "print configuration options"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_context"}
+ Outer_Syntax.command @{command_keyword print_context}
"print context of local theory target"
(Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
val _ =
- Outer_Syntax.command @{command_spec "print_theory"}
+ Outer_Syntax.command @{command_keyword print_theory}
"print logical theory contents"
(Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_syntax"}
+ Outer_Syntax.command @{command_keyword print_syntax}
"print inner syntax of context"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_defn_rules"}
+ Outer_Syntax.command @{command_keyword print_defn_rules}
"print definitional rewrite rules of context"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_abbrevs"}
+ Outer_Syntax.command @{command_keyword print_abbrevs}
"print constant abbreviations of context"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_theorems"}
+ Outer_Syntax.command @{command_keyword print_theorems}
"print theorems of local theory or proof context"
(Parse.opt_bang >> (fn b =>
Toplevel.unknown_context o
Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
val _ =
- Outer_Syntax.command @{command_spec "print_locales"}
+ Outer_Syntax.command @{command_keyword print_locales}
"print locales of this theory"
(Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_classes"}
+ Outer_Syntax.command @{command_keyword print_classes}
"print classes of this theory"
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Class.print_classes o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_locale"}
+ Outer_Syntax.command @{command_keyword print_locale}
"print locale of this theory"
(Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
Toplevel.unknown_theory o
Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
val _ =
- Outer_Syntax.command @{command_spec "print_interps"}
+ Outer_Syntax.command @{command_keyword print_interps}
"print interpretations of locale for this theory or proof context"
(Parse.position Parse.xname >> (fn name =>
Toplevel.unknown_context o
Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
val _ =
- Outer_Syntax.command @{command_spec "print_dependencies"}
+ Outer_Syntax.command @{command_keyword print_dependencies}
"print dependencies of locale expression"
(Parse.opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
Toplevel.unknown_context o
Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
val _ =
- Outer_Syntax.command @{command_spec "print_attributes"}
+ Outer_Syntax.command @{command_keyword print_attributes}
"print attributes of this theory"
(Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_simpset"}
+ Outer_Syntax.command @{command_keyword print_simpset}
"print context of Simplifier"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_rules"} "print intro/elim rules"
+ Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_methods"} "print methods of this theory"
+ Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory"
(Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_antiquotations"}
+ Outer_Syntax.command @{command_keyword print_antiquotations}
"print document antiquotations"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_ML_antiquotations"}
+ Outer_Syntax.command @{command_keyword print_ML_antiquotations}
"print ML antiquotations"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "thy_deps"} "visualize theory dependencies"
+ Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
(Scan.succeed Isar_Cmd.thy_deps);
val _ =
- Outer_Syntax.command @{command_spec "locale_deps"} "visualize locale dependencies"
+ Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
(Scan.succeed Isar_Cmd.locale_deps);
val _ =
- Outer_Syntax.command @{command_spec "print_term_bindings"}
+ Outer_Syntax.command @{command_keyword print_term_bindings}
"print term bindings of proof context"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep
(Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_facts"} "print facts of proof context"
+ Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_cases"} "print cases of proof context"
+ Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_statement"}
+ Outer_Syntax.command @{command_keyword print_statement}
"print theorems as long statements"
(opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
val _ =
- Outer_Syntax.command @{command_spec "thm"} "print theorems"
+ Outer_Syntax.command @{command_keyword thm} "print theorems"
(opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
val _ =
- Outer_Syntax.command @{command_spec "prf"} "print proof terms of theorems"
+ Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
(opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
val _ =
- Outer_Syntax.command @{command_spec "full_prf"} "print full proof terms of theorems"
+ Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
(opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
val _ =
- Outer_Syntax.command @{command_spec "prop"} "read and print proposition"
+ Outer_Syntax.command @{command_keyword prop} "read and print proposition"
(opt_modes -- Parse.term >> Isar_Cmd.print_prop);
val _ =
- Outer_Syntax.command @{command_spec "term"} "read and print term"
+ Outer_Syntax.command @{command_keyword term} "read and print term"
(opt_modes -- Parse.term >> Isar_Cmd.print_term);
val _ =
- Outer_Syntax.command @{command_spec "typ"} "read and print type"
+ Outer_Syntax.command @{command_keyword typ} "read and print type"
(opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
>> Isar_Cmd.print_type);
val _ =
- Outer_Syntax.command @{command_spec "print_codesetup"} "print code generator setup"
+ Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_state"}
+ Outer_Syntax.command @{command_keyword print_state}
"print current proof state (if present)"
(opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
val _ =
- Outer_Syntax.command @{command_spec "welcome"} "print welcome message"
+ Outer_Syntax.command @{command_keyword welcome} "print welcome message"
(Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
val _ =
- Outer_Syntax.command @{command_spec "display_drafts"}
+ Outer_Syntax.command @{command_keyword display_drafts}
"display raw source files with symbols"
(Scan.repeat1 Parse.path >> (fn names =>
Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
@@ -881,24 +881,24 @@
val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
val _ =
- Outer_Syntax.command @{command_spec "realizers"}
+ Outer_Syntax.command @{command_keyword realizers}
"specify realizers for primitive axioms / theorems, together with correctness proof"
(Scan.repeat1 (Parse.xname -- 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_spec "realizability"}
+ Outer_Syntax.command @{command_keyword realizability}
"add equations characterizing realizability"
(Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
val _ =
- Outer_Syntax.command @{command_spec "extract_type"}
+ Outer_Syntax.command @{command_keyword extract_type}
"add equations characterizing type of extracted program"
(Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
val _ =
- Outer_Syntax.command @{command_spec "extract"} "extract terms from proofs"
+ Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
(Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
@@ -907,7 +907,7 @@
(** end **)
val _ =
- Outer_Syntax.command @{command_spec "end"} "end context"
+ Outer_Syntax.command @{command_keyword end} "end context"
(Scan.succeed
(Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
Toplevel.end_proof (K Proof.end_notepad)));
--- a/src/Pure/ML/ml_antiquotations.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Mon Apr 06 17:06:48 2015 +0200
@@ -253,7 +253,7 @@
if Keyword.is_keyword (Thy_Header.get_keywords thy) name then
"Parse.$$$ " ^ ML_Syntax.print_string name
else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
- ML_Antiquotation.value @{binding command_spec}
+ ML_Antiquotation.value @{binding command_keyword}
(Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) =>
(case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
SOME markup =>
--- a/src/Pure/Tools/class_deps.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Pure/Tools/class_deps.ML Mon Apr 06 17:06:48 2015 +0200
@@ -46,7 +46,7 @@
|| (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
val _ =
- Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies"
+ Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
((Scan.option parse_sort_list -- Scan.option parse_sort_list) >> (fn (super, sub) =>
(Toplevel.unknown_theory o
Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) super sub))));
--- a/src/Pure/Tools/find_consts.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Pure/Tools/find_consts.ML Mon Apr 06 17:06:48 2015 +0200
@@ -151,7 +151,7 @@
|> #1;
val _ =
- Outer_Syntax.command @{command_spec "find_consts"}
+ Outer_Syntax.command @{command_keyword find_consts}
"find constants by name / type patterns"
(query >> (fn spec =>
Toplevel.keep (fn st =>
--- a/src/Pure/Tools/find_theorems.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML Mon Apr 06 17:06:48 2015 +0200
@@ -535,7 +535,7 @@
|> #1;
val _ =
- Outer_Syntax.command @{command_spec "find_theorems"}
+ Outer_Syntax.command @{command_keyword find_theorems}
"find theorems meeting specified criteria"
(options -- query >> (fn ((opt_lim, rem_dups), spec) =>
Toplevel.keep (fn st =>
--- a/src/Pure/Tools/named_theorems.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Pure/Tools/named_theorems.ML Mon Apr 06 17:06:48 2015 +0200
@@ -89,7 +89,7 @@
in (name, lthy') end;
val _ =
- Outer_Syntax.local_theory @{command_spec "named_theorems"}
+ Outer_Syntax.local_theory @{command_keyword named_theorems}
"declare named collection of theorems"
(Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
fold (fn (b, descr) => snd o declare b descr));
--- a/src/Pure/Tools/thm_deps.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Pure/Tools/thm_deps.ML Mon Apr 06 17:06:48 2015 +0200
@@ -44,7 +44,7 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"
+ Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
(Parse.xthms1 >> (fn args =>
Toplevel.unknown_theory o Toplevel.keep (fn state =>
thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
@@ -101,7 +101,7 @@
in rev thms' end;
val _ =
- Outer_Syntax.command @{command_spec "unused_thms"} "find unused theorems"
+ Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
(Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
Toplevel.keep (fn state =>
--- a/src/Sequents/prover.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Sequents/prover.ML Mon Apr 06 17:06:48 2015 +0200
@@ -68,7 +68,7 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "print_pack"} "print pack of classical rules"
+ Outer_Syntax.command @{command_keyword print_pack} "print pack of classical rules"
(Scan.succeed (Toplevel.keep (Pretty.writeln o pretty_pack o Toplevel.context_of)));
--- a/src/Tools/Code/code_haskell.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Tools/Code/code_haskell.ML Mon Apr 06 17:06:48 2015 +0200
@@ -516,7 +516,7 @@
#> fold (fold (Code_Target.add_reserved target) o snd) prelude_import_unqualified_constr);
val _ =
- Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
+ Outer_Syntax.command @{command_keyword code_monad} "define code syntax for monads"
(Parse.term -- Parse.name >> (fn (raw_bind, target) =>
Toplevel.theory (add_monad target raw_bind)));
--- a/src/Tools/Code/code_preproc.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML Mon Apr 06 17:06:48 2015 +0200
@@ -588,7 +588,7 @@
end);
val _ =
- Outer_Syntax.command @{command_spec "print_codeproc"} "print code preprocessor setup"
+ Outer_Syntax.command @{command_keyword print_codeproc} "print code preprocessor setup"
(Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of)));
end; (*struct*)
--- a/src/Tools/Code/code_runtime.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Tools/Code/code_runtime.ML Mon Apr 06 17:06:48 2015 +0200
@@ -475,7 +475,7 @@
in
val _ =
- Outer_Syntax.command @{command_spec "code_reflect"}
+ Outer_Syntax.command @{command_keyword code_reflect}
"enrich runtime environment with generated code"
(Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype
::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
--- a/src/Tools/Code/code_target.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Tools/Code/code_target.ML Mon Apr 06 17:06:48 2015 +0200
@@ -638,25 +638,25 @@
:|-- (fn (all_public, raw_cs) => (code_expr_checkingP all_public raw_cs || code_expr_inP all_public raw_cs));
val _ =
- Outer_Syntax.command @{command_spec "code_reserved"}
+ Outer_Syntax.command @{command_keyword code_reserved}
"declare words as reserved for target language"
(Parse.name -- Scan.repeat1 Parse.name
>> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
val _ =
- Outer_Syntax.command @{command_spec "code_identifier"} "declare mandatory names for code symbols"
+ Outer_Syntax.command @{command_keyword code_identifier} "declare mandatory names for code symbols"
(parse_symbol_pragmas Parse.name Parse.name Parse.name Parse.name Parse.name Parse.name
>> (Toplevel.theory o fold set_identifiers_cmd));
val _ =
- Outer_Syntax.command @{command_spec "code_printing"} "declare dedicated printing for code symbols"
+ Outer_Syntax.command @{command_keyword code_printing} "declare dedicated printing for code symbols"
(parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
(Parse.text -- Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [])
>> (Toplevel.theory o fold set_printings_cmd));
val _ =
- Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
+ Outer_Syntax.command @{command_keyword export_code} "generate executable code for constants"
(Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
end; (*struct*)
--- a/src/Tools/Code/code_thingol.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML Mon Apr 06 17:06:48 2015 +0200
@@ -957,14 +957,14 @@
in
val _ =
- Outer_Syntax.command @{command_spec "code_thms"}
+ Outer_Syntax.command @{command_keyword code_thms}
"print system of code equations for code"
(Scan.repeat1 Parse.term >> (fn cs =>
Toplevel.unknown_context o
Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs)));
val _ =
- Outer_Syntax.command @{command_spec "code_deps"}
+ Outer_Syntax.command @{command_keyword code_deps}
"visualize dependencies of code equations for code"
(Scan.repeat1 Parse.term >> (fn cs =>
Toplevel.unknown_context o
--- a/src/Tools/adhoc_overloading.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Tools/adhoc_overloading.ML Mon Apr 06 17:06:48 2015 +0200
@@ -233,12 +233,12 @@
end;
val _ =
- Outer_Syntax.local_theory @{command_spec "adhoc_overloading"}
+ Outer_Syntax.local_theory @{command_keyword adhoc_overloading}
"add adhoc overloading for constants / fixed variables"
(Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd true);
val _ =
- Outer_Syntax.local_theory @{command_spec "no_adhoc_overloading"}
+ Outer_Syntax.local_theory @{command_keyword no_adhoc_overloading}
"delete adhoc overloading for constants / fixed variables"
(Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd false);
--- a/src/Tools/induct.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Tools/induct.ML Mon Apr 06 17:06:48 2015 +0200
@@ -257,7 +257,7 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "print_induct_rules"}
+ Outer_Syntax.command @{command_keyword print_induct_rules}
"print induction and cases rules"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (print_rules o Toplevel.context_of)));
--- a/src/Tools/permanent_interpretation.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Tools/permanent_interpretation.ML Mon Apr 06 17:06:48 2015 +0200
@@ -95,7 +95,7 @@
end;
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
"prove interpretation of locale expression into named theory"
(Parse.!!! (Parse_Spec.locale_expression true) --
Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
--- a/src/Tools/quickcheck.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Tools/quickcheck.ML Mon Apr 06 17:06:48 2015 +0200
@@ -527,11 +527,11 @@
@{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed [];
val _ =
- Outer_Syntax.command @{command_spec "quickcheck_params"} "set parameters for random testing"
+ Outer_Syntax.command @{command_keyword quickcheck_params} "set parameters for random testing"
(parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
val _ =
- Outer_Syntax.command @{command_spec "quickcheck"}
+ Outer_Syntax.command @{command_keyword quickcheck}
"try to find counterexample for subgoal"
(parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
--- a/src/Tools/solve_direct.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Tools/solve_direct.ML Mon Apr 06 17:06:48 2015 +0200
@@ -92,7 +92,7 @@
val solve_direct = do_solve_direct Normal
val _ =
- Outer_Syntax.command @{command_spec "solve_direct"}
+ Outer_Syntax.command @{command_keyword solve_direct}
"try to solve conjectures directly with existing theorems"
(Scan.succeed (Toplevel.unknown_proof o
Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
--- a/src/Tools/subtyping.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Tools/subtyping.ML Mon Apr 06 17:06:48 2015 +0200
@@ -1115,7 +1115,7 @@
(* outer syntax commands *)
val _ =
- Outer_Syntax.command @{command_spec "print_coercions"}
+ Outer_Syntax.command @{command_keyword print_coercions}
"print information about coercions"
(Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)));
--- a/src/Tools/try.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Tools/try.ML Mon Apr 06 17:06:48 2015 +0200
@@ -75,7 +75,7 @@
|> tap (fn NONE => writeln "Tried in vain." | _ => ())
val _ =
- Outer_Syntax.command @{command_spec "try"}
+ Outer_Syntax.command @{command_keyword try}
"try a combination of automatic proving and disproving tools"
(Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
--- a/src/ZF/Tools/datatype_package.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/ZF/Tools/datatype_package.ML Mon Apr 06 17:06:48 2015 +0200
@@ -430,7 +430,7 @@
val _ =
Outer_Syntax.command
- (if coind then @{command_spec "codatatype"} else @{command_spec "datatype"})
+ (if coind then @{command_keyword codatatype} else @{command_keyword datatype})
("define " ^ coind_prefix ^ "datatype")
((Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
--- a/src/ZF/Tools/ind_cases.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/ZF/Tools/ind_cases.ML Mon Apr 06 17:06:48 2015 +0200
@@ -53,7 +53,7 @@
in thy |> Global_Theory.note_thmss "" facts |> snd end;
val _ =
- Outer_Syntax.command @{command_spec "inductive_cases"}
+ Outer_Syntax.command @{command_keyword inductive_cases}
"create simplified instances of elimination rules (improper)"
(Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
>> (Toplevel.theory o inductive_cases));
--- a/src/ZF/Tools/induct_tacs.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Mon Apr 06 17:06:48 2015 +0200
@@ -191,7 +191,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing set inductively"
+ Outer_Syntax.command @{command_keyword rep_datatype} "represent existing set inductively"
((@{keyword "elimination"} |-- Parse.!!! Parse.xthm) --
(@{keyword "induction"} |-- Parse.!!! Parse.xthm) --
(@{keyword "case_eqns"} |-- Parse.!!! Parse.xthms1) --
--- a/src/ZF/Tools/inductive_package.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/ZF/Tools/inductive_package.ML Mon Apr 06 17:06:48 2015 +0200
@@ -595,7 +595,7 @@
val _ =
Outer_Syntax.command
- (if coind then @{command_spec "coinductive"} else @{command_spec "inductive"})
+ (if coind then @{command_keyword coinductive} else @{command_keyword inductive})
("define " ^ co_prefix ^ "inductive sets") ind_decl;
end;
--- a/src/ZF/Tools/primrec_package.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/ZF/Tools/primrec_package.ML Mon Apr 06 17:06:48 2015 +0200
@@ -197,7 +197,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.command @{command_spec "primrec"} "define primitive recursive functions on datatypes"
+ Outer_Syntax.command @{command_keyword primrec} "define primitive recursive functions on datatypes"
(Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
>> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
--- a/src/ZF/Tools/typechk.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/ZF/Tools/typechk.ML Mon Apr 06 17:06:48 2015 +0200
@@ -126,7 +126,7 @@
"ZF type-checking");
val _ =
- Outer_Syntax.command @{command_spec "print_tcset"} "print context of ZF typecheck"
+ Outer_Syntax.command @{command_keyword print_tcset} "print context of ZF typecheck"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (print_tcset o Toplevel.context_of)));