--- 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 []) ([], [])) ([], ([], [])))
--- 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))
--- 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
--- 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)))
--- 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)));
--- 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;
--- 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 _ =
--- 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));
--- 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 _ =
--- 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)));
--- 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