tuned command descriptions
authorblanchet
Wed Oct 02 10:53:15 2013 +0200 (2013-10-02)
changeset 5402570bc41e7a91e
parent 54024 07ab4fd922c2
child 54026 82d9b2701a03
tuned command descriptions
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_lfp_compat.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Oct 02 10:39:01 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Oct 02 10:53:15 2013 +0200
     1.3 @@ -2914,7 +2914,7 @@
     1.4    end;
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
     1.8 +  Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes"
     1.9      (parse_co_datatype_cmd Greatest_FP construct_gfp);
    1.10  
    1.11  val option_parser = Parse.group (fn () => "option") (Parse.reserved "sequential" >> K true);
     2.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Oct 02 10:39:01 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Oct 02 10:53:15 2013 +0200
     2.3 @@ -1884,7 +1884,7 @@
     2.4    end;
     2.5  
     2.6  val _ =
     2.7 -  Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes"
     2.8 +  Outer_Syntax.local_theory @{command_spec "datatype_new"} "define new-style inductive datatypes"
     2.9      (parse_co_datatype_cmd Least_FP construct_lfp);
    2.10  
    2.11  val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"}
     3.1 --- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Wed Oct 02 10:39:01 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Wed Oct 02 10:53:15 2013 +0200
     3.3 @@ -166,7 +166,7 @@
     3.4  
     3.5  val _ =
     3.6    Outer_Syntax.local_theory @{command_spec "datatype_new_compat"}
     3.7 -    "register a new-style datatype as an old-style datatype"
     3.8 +    "register new-style datatypes as old-style datatypes"
     3.9      (Scan.repeat1 Parse.type_const >> datatype_new_compat_cmd);
    3.10  
    3.11  end;