# HG changeset patch
# User wenzelm
# Date 1279903355 -7200
# Node ID 4b7afae88c576c270fc85317a30bf163c5dec1d7
# Parent  3cbd7fa164b19e9fff5fa5f7ea611f16d57d8b89
observe standard conventions for doc-strings;

diff -r 3cbd7fa164b1 -r 4b7afae88c57 src/HOL/Boogie/Tools/boogie_commands.ML
--- 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))
 
diff -r 3cbd7fa164b1 -r 4b7afae88c57 src/HOL/Tools/Quotient/quotient_info.ML
--- 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 *)
diff -r 3cbd7fa164b1 -r 4b7afae88c57 src/Pure/codegen.ML
--- 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;