# HG changeset patch
# User blanchet
# Date 1380703995 -7200
# Node ID 70bc41e7a91e7a24ad3f9111fe0abb6183c5f277
# Parent  07ab4fd922c2ae1124f174bc175f303296650041
tuned command descriptions

diff -r 07ab4fd922c2 -r 70bc41e7a91e src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Oct 02 10:39:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Oct 02 10:53:15 2013 +0200
@@ -2914,7 +2914,7 @@
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
+  Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes"
     (parse_co_datatype_cmd Greatest_FP construct_gfp);
 
 val option_parser = Parse.group (fn () => "option") (Parse.reserved "sequential" >> K true);
diff -r 07ab4fd922c2 -r 70bc41e7a91e src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Oct 02 10:39:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Oct 02 10:53:15 2013 +0200
@@ -1884,7 +1884,7 @@
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes"
+  Outer_Syntax.local_theory @{command_spec "datatype_new"} "define new-style inductive datatypes"
     (parse_co_datatype_cmd Least_FP construct_lfp);
 
 val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"}
diff -r 07ab4fd922c2 -r 70bc41e7a91e src/HOL/BNF/Tools/bnf_lfp_compat.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Wed Oct 02 10:39:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Wed Oct 02 10:53:15 2013 +0200
@@ -166,7 +166,7 @@
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "datatype_new_compat"}
-    "register a new-style datatype as an old-style datatype"
+    "register new-style datatypes as old-style datatypes"
     (Scan.repeat1 Parse.type_const >> datatype_new_compat_cmd);
 
 end;