# HG changeset patch # User wenzelm # Date 1428332808 -7200 # Node ID b8ffc3dc9e24fefe2af58f52b7e1e7609970c97a # Parent 343905de27b19a718bf665be44a40a0f011d3f3e @{command_spec} is superseded by @{command_keyword}; diff -r 343905de27b1 -r b8ffc3dc9e24 NEWS --- 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 *** diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Decision_Procs/approximation.ML --- 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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/HOLCF/Tools/Domain/domain.ML --- 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 diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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 diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/HOLCF/Tools/cpodef.ML --- 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)) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/HOLCF/Tools/domaindef.ML --- 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 diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/HOLCF/Tools/fixrec.ML --- 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)) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Import/import_data.ML --- 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))) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Import/import_rule.ML --- 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))) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Library/Old_SMT/old_smt_config.ML --- 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))) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Library/bnf_axiomatization.ML --- 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)); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Library/code_test.ML --- 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))) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Library/refute.ML --- 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 => diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Library/simps_case_conv.ML --- 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) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Nominal/nominal_atoms.ML --- 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; diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Nominal/nominal_datatype.ML --- 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)); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Nominal/nominal_inductive.ML --- 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)); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Nominal/nominal_inductive2.ML --- 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 ")"})) -- diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Nominal/nominal_primrec.ML --- 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) => diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Orderings.thy --- 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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/SMT_Examples/boogie.ML --- 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 => diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/SPARK/Tools/spark_commands.ML --- 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 >> diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Statespace/state_space.ML --- 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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- 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 diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML --- 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 diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/BNF/bnf_def.ML --- 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 -- diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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 diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/BNF/bnf_gfp.ML --- 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}); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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 ")"}) []) -- diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/BNF/bnf_lfp.ML --- 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}); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- 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); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- 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 ")"}) []) -- diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Ctr_Sugar/case_translation.ML --- 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))) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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 diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Function/fun.ML --- 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)) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Function/fun_cases.ML --- 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)); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Function/function.ML --- 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) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Function/partial_function.ML --- 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)); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Lifting/lifting_def.ML --- 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) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Lifting/lifting_info.ML --- 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 diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Lifting/lifting_setup.ML --- 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) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Nitpick/nitpick_commands.ML --- 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) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Old_Datatype/old_datatype.ML --- 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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Old_Datatype/old_rep_datatype.ML --- 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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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))) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- 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 diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Quickcheck/abstract_generators.ML --- 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)) -- diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Quickcheck/find_unused_assms.ML --- 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))) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Quotient/quotient_def.ML --- 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) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Quotient/quotient_info.ML --- 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; diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Quotient/quotient_type.ML --- 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) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/SMT/smt_config.ML --- 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))) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/choice_specification.ML --- 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))) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/functor.ML --- 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)); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/inductive.ML --- 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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/inductive_set.ML --- 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; diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/recdef.ML --- 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 ")"}) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/record.ML --- 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) diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/try0.ML --- 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 ([], [], [], []); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/typedef.ML --- 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) -- diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/value.ML --- 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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/ex/Cartouche_Examples.thy --- 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 \Outer syntax: cartouche within command syntax\ ML \ - Outer_Syntax.command @{command_spec "cartouche"} "" + Outer_Syntax.command @{command_keyword cartouche} "" (Parse.cartouche >> (fn s => Toplevel.imperative (fn () => writeln s))) \ @@ -116,7 +116,7 @@ subsubsection \Term cartouche and regular quotes\ ML \ - 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 \ Outer_Syntax.command - @{command_spec "text_cartouche"} "" + @{command_keyword text_cartouche} "" (Parse.opt_target -- Parse.input Parse.cartouche >> Thy_Output.document_command) \ diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/ex/Commands.thy --- 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 \Diagnostic command: no state change\ ML \ - 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 \Old-style global theory declaration\ ML \ - 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 \Local theory specification\ ML \ - 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; diff -r 343905de27b1 -r b8ffc3dc9e24 src/Provers/classical.ML --- 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; diff -r 343905de27b1 -r b8ffc3dc9e24 src/Pure/Isar/calculation.ML --- 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; diff -r 343905de27b1 -r b8ffc3dc9e24 src/Pure/Isar/isar_syn.ML --- 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 "\"} || @{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 "\"} || @{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 "\"} || @{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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/Pure/ML/ml_antiquotations.ML --- 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 => diff -r 343905de27b1 -r b8ffc3dc9e24 src/Pure/Tools/class_deps.ML --- 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)))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/Pure/Tools/find_consts.ML --- 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 => diff -r 343905de27b1 -r b8ffc3dc9e24 src/Pure/Tools/find_theorems.ML --- 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 => diff -r 343905de27b1 -r b8ffc3dc9e24 src/Pure/Tools/named_theorems.ML --- 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)); diff -r 343905de27b1 -r b8ffc3dc9e24 src/Pure/Tools/thm_deps.ML --- 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 => diff -r 343905de27b1 -r b8ffc3dc9e24 src/Sequents/prover.ML --- 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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/Tools/Code/code_haskell.ML --- 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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/Tools/Code/code_preproc.ML --- 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*) diff -r 343905de27b1 -r b8ffc3dc9e24 src/Tools/Code/code_runtime.ML --- 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))) [] diff -r 343905de27b1 -r b8ffc3dc9e24 src/Tools/Code/code_target.ML --- 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*) diff -r 343905de27b1 -r b8ffc3dc9e24 src/Tools/Code/code_thingol.ML --- 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 diff -r 343905de27b1 -r b8ffc3dc9e24 src/Tools/adhoc_overloading.ML --- 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); diff -r 343905de27b1 -r b8ffc3dc9e24 src/Tools/induct.ML --- 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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/Tools/permanent_interpretation.ML --- 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 ":" diff -r 343905de27b1 -r b8ffc3dc9e24 src/Tools/quickcheck.ML --- 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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/Tools/solve_direct.ML --- 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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/Tools/subtyping.ML --- 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))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/Tools/try.ML --- 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))) diff -r 343905de27b1 -r b8ffc3dc9e24 src/ZF/Tools/datatype_package.ML --- 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 "\"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") -- Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) -- diff -r 343905de27b1 -r b8ffc3dc9e24 src/ZF/Tools/ind_cases.ML --- 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)); diff -r 343905de27b1 -r b8ffc3dc9e24 src/ZF/Tools/induct_tacs.ML --- 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) -- diff -r 343905de27b1 -r b8ffc3dc9e24 src/ZF/Tools/inductive_package.ML --- 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; diff -r 343905de27b1 -r b8ffc3dc9e24 src/ZF/Tools/primrec_package.ML --- 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)))); diff -r 343905de27b1 -r b8ffc3dc9e24 src/ZF/Tools/typechk.ML --- 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)));