# HG changeset patch # User wenzelm # Date 1353937408 -3600 # Node ID 67fb9a168d1051f36d9a4940ca693775daed0360 # Parent 7b73c050983513e39c1e5f911438ee747074e2c8 tuned command descriptions; diff -r 7b73c0509835 -r 67fb9a168d10 src/HOL/BNF/Tools/bnf_wrap.ML --- a/src/HOL/BNF/Tools/bnf_wrap.ML Mon Nov 26 13:54:43 2012 +0100 +++ b/src/HOL/BNF/Tools/bnf_wrap.ML Mon Nov 26 14:43:28 2012 +0100 @@ -675,7 +675,7 @@ >> (pairself (exists I) o split_list)) (false, false); val _ = - Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype" + Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wrap an existing datatype" ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss -- Scan.optional parse_bound_termss []) ([], [])) ([], ([], []))) diff -r 7b73c0509835 -r 67fb9a168d10 src/HOL/Boogie/Tools/boogie_commands.ML --- a/src/HOL/Boogie/Tools/boogie_commands.ML Mon Nov 26 13:54:43 2012 +0100 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Mon Nov 26 14:43:28 2012 +0100 @@ -302,7 +302,7 @@ val _ = Outer_Syntax.command @{command_spec "boogie_vc"} - "enter into proof mode for a specific verification condition" + "enter into proof mode for a specific Boogie verification condition" (vc_name -- vc_opts >> (fn args => (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args)))) @@ -334,7 +334,7 @@ val _ = Outer_Syntax.improper_command @{command_spec "boogie_status"} - "show the name and state of all loaded verification conditions" + "show the name and state of all loaded Boogie verification conditions" (status_test >> status_cmd || status_vc >> status_cmd || Scan.succeed (status_cmd boogie_status)) diff -r 7b73c0509835 -r 67fb9a168d10 src/HOL/Import/import_data.ML --- a/src/HOL/Import/import_data.ML Mon Nov 26 13:54:43 2012 +0100 +++ b/src/HOL/Import/import_data.ML Mon Nov 26 14:43:28 2012 +0100 @@ -104,13 +104,13 @@ val type_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >> (fn (ty_name1, ty_name2) => add_typ_map ty_name1 ty_name2) val _ = Outer_Syntax.command @{command_spec "import_type_map"} - "Map external type name to existing Isabelle/HOL type name" + "map external type name to existing Isabelle/HOL type name" (type_map >> Toplevel.theory) val const_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >> (fn (cname1, cname2) => add_const_map cname1 cname2) val _ = Outer_Syntax.command @{command_spec "import_const_map"} - "Map external const name to existing Isabelle/HOL const name" + "map external const name to existing Isabelle/HOL const name" (const_map >> Toplevel.theory) (* Initial type and constant maps, for types and constants that are not diff -r 7b73c0509835 -r 67fb9a168d10 src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Mon Nov 26 13:54:43 2012 +0100 +++ b/src/HOL/Import/import_rule.ML Mon Nov 26 14:43:28 2012 +0100 @@ -443,7 +443,7 @@ (thy, init_state) |> File.fold_lines process_line path |> fst val _ = Outer_Syntax.command @{command_spec "import_file"} - "Import a recorded proof file" + "import a recorded proof file" (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy))) diff -r 7b73c0509835 -r 67fb9a168d10 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Mon Nov 26 13:54:43 2012 +0100 +++ b/src/HOL/Statespace/state_space.ML Mon Nov 26 14:43:28 2012 +0100 @@ -706,7 +706,7 @@ (plus1_unless comp parent -- Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) []))); val _ = - Outer_Syntax.command @{command_spec "statespace"} "define state space" + Outer_Syntax.command @{command_spec "statespace"} "define state-space as locale context" (statespace_decl >> (fn ((args, name), (parents, comps)) => Toplevel.theory (define_statespace args name parents comps))); diff -r 7b73c0509835 -r 67fb9a168d10 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Nov 26 13:54:43 2012 +0100 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Nov 26 14:43:28 2012 +0100 @@ -266,7 +266,7 @@ val _ = Outer_Syntax.local_theory @{command_spec "setup_lifting"} - "Setup lifting infrastructure" + "setup lifting infrastructure" (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> (fn ((gen_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_code xthm opt_reflp_xthm)) end; diff -r 7b73c0509835 -r 67fb9a168d10 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Mon Nov 26 13:54:43 2012 +0100 +++ b/src/HOL/Tools/inductive.ML Mon Nov 26 14:43:28 2012 +0100 @@ -1157,7 +1157,7 @@ val _ = Outer_Syntax.local_theory @{command_spec "inductive_cases"} - "create simplified instances of elimination rules (improper)" + "create simplified instances of elimination rules" (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases)); val _ = diff -r 7b73c0509835 -r 67fb9a168d10 src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Mon Nov 26 13:54:43 2012 +0100 +++ b/src/HOL/Tools/recdef.ML Mon Nov 26 14:43:28 2012 +0100 @@ -302,7 +302,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 (TFL)" + Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (obsolete TFL)" (recdef_decl >> Toplevel.theory); @@ -314,12 +314,12 @@ val _ = Outer_Syntax.command @{command_spec "defer_recdef"} - "defer general recursive functions (TFL)" + "defer general recursive functions (obsolete TFL)" (defer_recdef_decl >> Toplevel.theory); val _ = Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"} - "recommence proof of termination condition (TFL)" + "recommence proof of termination condition (obsolete TFL)" ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname -- Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"}) >> (fn ((thm_name, name), i) => recdef_tc thm_name name i)); diff -r 7b73c0509835 -r 67fb9a168d10 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Nov 26 13:54:43 2012 +0100 +++ b/src/Pure/Isar/isar_syn.ML Mon Nov 26 14:43:28 2012 +0100 @@ -134,11 +134,11 @@ Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default; val _ = - Outer_Syntax.command @{command_spec "syntax"} "declare syntactic constants" + Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses" (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax)); val _ = - Outer_Syntax.command @{command_spec "no_syntax"} "delete syntax declarations" + Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses" (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax)); @@ -159,11 +159,11 @@ >> (fn (left, (arr, right)) => arr (left, right)); val _ = - Outer_Syntax.command @{command_spec "translations"} "declare syntax translation rules" + Outer_Syntax.command @{command_spec "translations"} "add syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations)); val _ = - Outer_Syntax.command @{command_spec "no_translations"} "remove syntax translation rules" + Outer_Syntax.command @{command_spec "no_translations"} "delete syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations)); @@ -538,7 +538,7 @@ (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have)); val _ = - Outer_Syntax.command @{command_spec "hence"} "abbreviates \"then have\"" + Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\"" (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence)); val _ = @@ -547,7 +547,7 @@ (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show)); val _ = - Outer_Syntax.command @{command_spec "thus"} "abbreviates \"then show\"" + Outer_Syntax.command @{command_spec "thus"} "old-style alias of \"then show\"" (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus)); @@ -595,7 +595,7 @@ (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd))); val _ = - Outer_Syntax.command @{command_spec "def"} "local definition" + Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)" (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- ((Parse.binding -- Parse.opt_mixfix) -- @@ -649,7 +649,7 @@ (* end proof *) val _ = - Outer_Syntax.command @{command_spec "qed"} "conclude (sub-)proof" + Outer_Syntax.command @{command_spec "qed"} "conclude proof" (Scan.option Method.parse >> Isar_Cmd.qed); val _ = @@ -692,11 +692,11 @@ (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results))); val _ = - Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement (unstructured)" + Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)" (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results))); val _ = - Outer_Syntax.command @{command_spec "proof"} "backward proof" + Outer_Syntax.command @{command_spec "proof"} "backward proof step" (Scan.option Method.parse >> (fn m => Toplevel.print o Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o Toplevel.skip_proof (fn i => i + 1))); @@ -741,7 +741,7 @@ (Position.of_properties (Position.default_properties pos props), str)); val _ = - Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "nested Isabelle command" + Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "evaluate nested Isabelle command" (props_text :|-- (fn (pos, str) => (case Outer_Syntax.parse pos str of [tr] => Scan.succeed (K tr) @@ -851,8 +851,7 @@ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods)); val _ = - Outer_Syntax.improper_command @{command_spec "print_antiquotations"} - "print antiquotations (global)" + Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations" (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations)); val _ = @@ -986,7 +985,7 @@ val _ = Outer_Syntax.improper_command @{command_spec "commit"} - "commit current session to ML database" + "commit current session to ML session image" (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit)); val _ = diff -r 7b73c0509835 -r 67fb9a168d10 src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Mon Nov 26 13:54:43 2012 +0100 +++ b/src/Pure/Tools/find_consts.ML Mon Nov 26 14:43:28 2012 +0100 @@ -136,7 +136,8 @@ in val _ = - Outer_Syntax.improper_command @{command_spec "find_consts"} "search constants by type pattern" + Outer_Syntax.improper_command @{command_spec "find_consts"} + "find constants by name/type patterns" (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion) >> (fn spec => Toplevel.no_timing o Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec))); diff -r 7b73c0509835 -r 67fb9a168d10 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Mon Nov 26 13:54:43 2012 +0100 +++ b/src/Pure/Tools/find_theorems.ML Mon Nov 26 14:43:28 2012 +0100 @@ -625,7 +625,7 @@ val _ = Outer_Syntax.improper_command @{command_spec "find_theorems"} - "print theorems meeting specified criteria" + "find theorems meeting specified criteria" (options -- query_parser >> (fn ((opt_lim, rem_dups), spec) => Toplevel.no_timing o