--- a/src/HOL/Boogie/Tools/boogie_commands.ML Thu Jul 22 23:29:39 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Fri Jul 23 18:42:35 2010 +0200
@@ -268,7 +268,7 @@
val _ =
Outer_Syntax.command "boogie_open"
- "Open a new Boogie environment and load a Boogie-generated .b2i file."
+ "open a new Boogie environment and load a Boogie-generated .b2i file"
Keyword.thy_decl
(scan_opt "quiet" -- Parse.name -- vc_offsets >>
(Toplevel.theory o boogie_open))
@@ -296,7 +296,7 @@
val _ =
Outer_Syntax.command "boogie_vc"
- "Enter into proof mode for a specific verification condition."
+ "enter into proof mode for a specific verification condition"
Keyword.thy_goal
(vc_name -- vc_opts >> (fn args =>
(Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
@@ -329,7 +329,7 @@
val _ =
Outer_Syntax.improper_command "boogie_status"
- "Show the name and state of all loaded verification conditions."
+ "show the name and state of all loaded verification conditions"
Keyword.diag
(status_test >> status_cmd ||
status_vc >> status_cmd ||
@@ -338,7 +338,7 @@
val _ =
Outer_Syntax.command "boogie_end"
- "Close the current Boogie environment."
+ "close the current Boogie environment"
Keyword.thy_decl
(Scan.succeed (Toplevel.theory boogie_end))
--- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Jul 22 23:29:39 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Jul 23 18:42:35 2010 +0200
@@ -282,9 +282,9 @@
Keyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
val _ = map improper_command
- [(print_mapsinfo, "print_quotmaps", "prints out all map functions"),
- (print_quotinfo, "print_quotients", "prints out all quotients"),
- (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
+ [(print_mapsinfo, "print_quotmaps", "print out all map functions"),
+ (print_quotinfo, "print_quotients", "print out all quotients"),
+ (print_qconstinfo, "print_quotconsts", "print out all quotient constants")]
end; (* structure *)
--- a/src/Pure/codegen.ML Thu Jul 22 23:29:39 2010 +0200
+++ b/src/Pure/codegen.ML Fri Jul 23 18:42:35 2010 +0200
@@ -1019,12 +1019,12 @@
val _ =
Outer_Syntax.command "code_library"
- "generates code for terms (one structure for each theory)" Keyword.thy_decl
+ "generate code for terms (one structure for each theory)" Keyword.thy_decl
(parse_code true);
val _ =
Outer_Syntax.command "code_module"
- "generates code for terms (single structure, incremental)" Keyword.thy_decl
+ "generate code for terms (single structure, incremental)" Keyword.thy_decl
(parse_code false);
end;