src/HOL/Boogie/Tools/boogie_commands.ML

 val vc_offsets = Scan.optional (Args.bracks (Parse.list1
   (Parse.string --| Args.colon -- Parse.nat))) []
 
 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))
 
 

     scan_val "without" vc_labels >> VC_Without) ||
   Scan.succeed VC_Complete
 
 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))))
 
 

 fun status_cmd f = Toplevel.no_timing o Toplevel.keep (fn state =>
   f (Toplevel.theory_of state))
 
 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 ||
      Scan.succeed (status_cmd boogie_status))
 
 
 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))
 
 
 val setup = Theory.at_end (fn thy =>