tuned command descriptions;
authorwenzelm
Mon Nov 26 14:43:28 2012 +0100 (2012-11-26)
changeset 5021467fb9a168d10
parent 50213 7b73c0509835
child 50215 97959912840a
tuned command descriptions;
src/HOL/BNF/Tools/bnf_wrap.ML
src/HOL/Boogie/Tools/boogie_commands.ML
src/HOL/Import/import_data.ML
src/HOL/Import/import_rule.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/recdef.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_wrap.ML	Mon Nov 26 13:54:43 2012 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Mon Nov 26 14:43:28 2012 +0100
     1.3 @@ -675,7 +675,7 @@
     1.4      >> (pairself (exists I) o split_list)) (false, false);
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype"
     1.8 +  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wrap an existing datatype"
     1.9      ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) --
    1.10        Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
    1.11          Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
     2.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Mon Nov 26 13:54:43 2012 +0100
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Mon Nov 26 14:43:28 2012 +0100
     2.3 @@ -302,7 +302,7 @@
     2.4  
     2.5  val _ =
     2.6    Outer_Syntax.command @{command_spec "boogie_vc"}
     2.7 -    "enter into proof mode for a specific verification condition"
     2.8 +    "enter into proof mode for a specific Boogie verification condition"
     2.9      (vc_name -- vc_opts >> (fn args =>
    2.10        (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
    2.11  
    2.12 @@ -334,7 +334,7 @@
    2.13  
    2.14  val _ =
    2.15    Outer_Syntax.improper_command @{command_spec "boogie_status"}
    2.16 -    "show the name and state of all loaded verification conditions"
    2.17 +    "show the name and state of all loaded Boogie verification conditions"
    2.18      (status_test >> status_cmd ||
    2.19       status_vc >> status_cmd ||
    2.20       Scan.succeed (status_cmd boogie_status))
     3.1 --- a/src/HOL/Import/import_data.ML	Mon Nov 26 13:54:43 2012 +0100
     3.2 +++ b/src/HOL/Import/import_data.ML	Mon Nov 26 14:43:28 2012 +0100
     3.3 @@ -104,13 +104,13 @@
     3.4  val type_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >>
     3.5    (fn (ty_name1, ty_name2) => add_typ_map ty_name1 ty_name2)
     3.6  val _ = Outer_Syntax.command @{command_spec "import_type_map"}
     3.7 -  "Map external type name to existing Isabelle/HOL type name"
     3.8 +  "map external type name to existing Isabelle/HOL type name"
     3.9    (type_map >> Toplevel.theory)
    3.10  
    3.11  val const_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >>
    3.12    (fn (cname1, cname2) => add_const_map cname1 cname2)
    3.13  val _ = Outer_Syntax.command @{command_spec "import_const_map"}
    3.14 -  "Map external const name to existing Isabelle/HOL const name"
    3.15 +  "map external const name to existing Isabelle/HOL const name"
    3.16    (const_map >> Toplevel.theory)
    3.17  
    3.18  (* Initial type and constant maps, for types and constants that are not
     4.1 --- a/src/HOL/Import/import_rule.ML	Mon Nov 26 13:54:43 2012 +0100
     4.2 +++ b/src/HOL/Import/import_rule.ML	Mon Nov 26 14:43:28 2012 +0100
     4.3 @@ -443,7 +443,7 @@
     4.4    (thy, init_state) |> File.fold_lines process_line path |> fst
     4.5  
     4.6  val _ = Outer_Syntax.command @{command_spec "import_file"}
     4.7 -  "Import a recorded proof file"
     4.8 +  "import a recorded proof file"
     4.9    (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
    4.10  
    4.11  
     5.1 --- a/src/HOL/Statespace/state_space.ML	Mon Nov 26 13:54:43 2012 +0100
     5.2 +++ b/src/HOL/Statespace/state_space.ML	Mon Nov 26 14:43:28 2012 +0100
     5.3 @@ -706,7 +706,7 @@
     5.4          (plus1_unless comp parent --
     5.5            Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
     5.6  val _ =
     5.7 -  Outer_Syntax.command @{command_spec "statespace"} "define state space"
     5.8 +  Outer_Syntax.command @{command_spec "statespace"} "define state-space as locale context"
     5.9      (statespace_decl >> (fn ((args, name), (parents, comps)) =>
    5.10        Toplevel.theory (define_statespace args name parents comps)));
    5.11  
     6.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Nov 26 13:54:43 2012 +0100
     6.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Nov 26 14:43:28 2012 +0100
     6.3 @@ -266,7 +266,7 @@
     6.4  
     6.5  val _ = 
     6.6    Outer_Syntax.local_theory @{command_spec "setup_lifting"}
     6.7 -    "Setup lifting infrastructure" 
     6.8 +    "setup lifting infrastructure" 
     6.9        (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> 
    6.10          (fn ((gen_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_code xthm opt_reflp_xthm))
    6.11  end;
     7.1 --- a/src/HOL/Tools/inductive.ML	Mon Nov 26 13:54:43 2012 +0100
     7.2 +++ b/src/HOL/Tools/inductive.ML	Mon Nov 26 14:43:28 2012 +0100
     7.3 @@ -1157,7 +1157,7 @@
     7.4  
     7.5  val _ =
     7.6    Outer_Syntax.local_theory @{command_spec "inductive_cases"}
     7.7 -    "create simplified instances of elimination rules (improper)"
     7.8 +    "create simplified instances of elimination rules"
     7.9      (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
    7.10  
    7.11  val _ =
     8.1 --- a/src/HOL/Tools/recdef.ML	Mon Nov 26 13:54:43 2012 +0100
     8.2 +++ b/src/HOL/Tools/recdef.ML	Mon Nov 26 14:43:28 2012 +0100
     8.3 @@ -302,7 +302,7 @@
     8.4    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
     8.5  
     8.6  val _ =
     8.7 -  Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (TFL)"
     8.8 +  Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (obsolete TFL)"
     8.9      (recdef_decl >> Toplevel.theory);
    8.10  
    8.11  
    8.12 @@ -314,12 +314,12 @@
    8.13  
    8.14  val _ =
    8.15    Outer_Syntax.command @{command_spec "defer_recdef"}
    8.16 -    "defer general recursive functions (TFL)"
    8.17 +    "defer general recursive functions (obsolete TFL)"
    8.18      (defer_recdef_decl >> Toplevel.theory);
    8.19  
    8.20  val _ =
    8.21    Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"}
    8.22 -    "recommence proof of termination condition (TFL)"
    8.23 +    "recommence proof of termination condition (obsolete TFL)"
    8.24      ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
    8.25          Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
    8.26        >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
     9.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Nov 26 13:54:43 2012 +0100
     9.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 26 14:43:28 2012 +0100
     9.3 @@ -134,11 +134,11 @@
     9.4    Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default;
     9.5  
     9.6  val _ =
     9.7 -  Outer_Syntax.command @{command_spec "syntax"} "declare syntactic constants"
     9.8 +  Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses"
     9.9      (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
    9.10  
    9.11  val _ =
    9.12 -  Outer_Syntax.command @{command_spec "no_syntax"} "delete syntax declarations"
    9.13 +  Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses"
    9.14      (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));
    9.15  
    9.16  
    9.17 @@ -159,11 +159,11 @@
    9.18      >> (fn (left, (arr, right)) => arr (left, right));
    9.19  
    9.20  val _ =
    9.21 -  Outer_Syntax.command @{command_spec "translations"} "declare syntax translation rules"
    9.22 +  Outer_Syntax.command @{command_spec "translations"} "add syntax translation rules"
    9.23      (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
    9.24  
    9.25  val _ =
    9.26 -  Outer_Syntax.command @{command_spec "no_translations"} "remove syntax translation rules"
    9.27 +  Outer_Syntax.command @{command_spec "no_translations"} "delete syntax translation rules"
    9.28      (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
    9.29  
    9.30  
    9.31 @@ -538,7 +538,7 @@
    9.32      (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
    9.33  
    9.34  val _ =
    9.35 -  Outer_Syntax.command @{command_spec "hence"} "abbreviates \"then have\""
    9.36 +  Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\""
    9.37      (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
    9.38  
    9.39  val _ =
    9.40 @@ -547,7 +547,7 @@
    9.41      (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
    9.42  
    9.43  val _ =
    9.44 -  Outer_Syntax.command @{command_spec "thus"} "abbreviates \"then show\""
    9.45 +  Outer_Syntax.command @{command_spec "thus"} "old-style alias of  \"then show\""
    9.46      (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
    9.47  
    9.48  
    9.49 @@ -595,7 +595,7 @@
    9.50      (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
    9.51  
    9.52  val _ =
    9.53 -  Outer_Syntax.command @{command_spec "def"} "local definition"
    9.54 +  Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)"
    9.55      (Parse.and_list1
    9.56        (Parse_Spec.opt_thm_name ":" --
    9.57          ((Parse.binding -- Parse.opt_mixfix) --
    9.58 @@ -649,7 +649,7 @@
    9.59  (* end proof *)
    9.60  
    9.61  val _ =
    9.62 -  Outer_Syntax.command @{command_spec "qed"} "conclude (sub-)proof"
    9.63 +  Outer_Syntax.command @{command_spec "qed"} "conclude proof"
    9.64      (Scan.option Method.parse >> Isar_Cmd.qed);
    9.65  
    9.66  val _ =
    9.67 @@ -692,11 +692,11 @@
    9.68      (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results)));
    9.69  
    9.70  val _ =
    9.71 -  Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement (unstructured)"
    9.72 +  Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
    9.73      (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results)));
    9.74  
    9.75  val _ =
    9.76 -  Outer_Syntax.command @{command_spec "proof"} "backward proof"
    9.77 +  Outer_Syntax.command @{command_spec "proof"} "backward proof step"
    9.78      (Scan.option Method.parse >> (fn m => Toplevel.print o
    9.79        Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
    9.80        Toplevel.skip_proof (fn i => i + 1)));
    9.81 @@ -741,7 +741,7 @@
    9.82        (Position.of_properties (Position.default_properties pos props), str));
    9.83  
    9.84  val _ =
    9.85 -  Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "nested Isabelle command"
    9.86 +  Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "evaluate nested Isabelle command"
    9.87      (props_text :|-- (fn (pos, str) =>
    9.88        (case Outer_Syntax.parse pos str of
    9.89          [tr] => Scan.succeed (K tr)
    9.90 @@ -851,8 +851,7 @@
    9.91      (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods));
    9.92  
    9.93  val _ =
    9.94 -  Outer_Syntax.improper_command @{command_spec "print_antiquotations"}
    9.95 -    "print antiquotations (global)"
    9.96 +  Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations"
    9.97      (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations));
    9.98  
    9.99  val _ =
   9.100 @@ -986,7 +985,7 @@
   9.101  
   9.102  val _ =
   9.103    Outer_Syntax.improper_command @{command_spec "commit"}
   9.104 -    "commit current session to ML database"
   9.105 +    "commit current session to ML session image"
   9.106      (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
   9.107  
   9.108  val _ =
    10.1 --- a/src/Pure/Tools/find_consts.ML	Mon Nov 26 13:54:43 2012 +0100
    10.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Nov 26 14:43:28 2012 +0100
    10.3 @@ -136,7 +136,8 @@
    10.4  in
    10.5  
    10.6  val _ =
    10.7 -  Outer_Syntax.improper_command @{command_spec "find_consts"} "search constants by type pattern"
    10.8 +  Outer_Syntax.improper_command @{command_spec "find_consts"}
    10.9 +    "find constants by name/type patterns"
   10.10      (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
   10.11        >> (fn spec => Toplevel.no_timing o
   10.12          Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
    11.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Nov 26 13:54:43 2012 +0100
    11.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Nov 26 14:43:28 2012 +0100
    11.3 @@ -625,7 +625,7 @@
    11.4  
    11.5  val _ =
    11.6    Outer_Syntax.improper_command @{command_spec "find_theorems"}
    11.7 -    "print theorems meeting specified criteria"
    11.8 +    "find theorems meeting specified criteria"
    11.9      (options -- query_parser
   11.10        >> (fn ((opt_lim, rem_dups), spec) =>
   11.11          Toplevel.no_timing o