1.1 --- a/src/Provers/splitter.ML	Thu Sep 07 20:56:04 2000 +0200
     1.2 +++ b/src/Provers/splitter.ML	Thu Sep 07 20:56:58 2000 +0200
     1.3 @@ -430,7 +430,7 @@
     1.4  (** theory setup **)
     1.5  
     1.6  val setup =
     1.7 - [Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")],
     1.8 -  Method.add_methods [(splitN, split_meth oo split_args, "apply splitter rule")]];
     1.9 + [Attrib.add_attributes [(splitN, split_attr, "declaration of case split rule")],
    1.10 +  Method.add_methods [(splitN, split_meth oo split_args, "apply case split rule")]];
    1.11  
    1.12  end;

     2.1 --- a/src/Pure/Isar/calculation.ML	Thu Sep 07 20:56:04 2000 +0200
     2.2 +++ b/src/Pure/Isar/calculation.ML	Thu Sep 07 20:56:58 2000 +0200
     2.3 @@ -177,7 +177,7 @@
     2.4  (** theory setup **)
     2.5  
     2.6  val setup = [GlobalCalculation.init, LocalCalculation.init,
     2.7 -  Attrib.add_attributes [("trans", trans_attr, "declare transitivity rule")]];
     2.8 +  Attrib.add_attributes [("trans", trans_attr, "declaration of transitivity rule")]];
     2.9  
    2.10  
    2.11  end;

     3.1 --- a/src/Pure/Isar/method.ML	Thu Sep 07 20:56:04 2000 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Thu Sep 07 20:56:58 2000 +0200
     3.3 @@ -203,10 +203,14 @@
     3.4  (* concrete syntax *)
     3.5  
     3.6  val rule_atts =
     3.7 - [("dest", (Attrib.no_args dest_global, Attrib.no_args dest_local), "declare destruction rule"),
     3.8 -  ("elim", (Attrib.no_args elim_global, Attrib.no_args elim_local), "declare elimination rule"),
     3.9 -  ("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local), "declare introduction rule"),
    3.10 -  ("delrule", (Attrib.no_args delrule_global, Attrib.no_args delrule_local), "undeclare rule")];
    3.11 + [("dest", (Attrib.no_args dest_global, Attrib.no_args dest_local),
    3.12 +    "declaration of destruction rule"),
    3.13 +  ("elim", (Attrib.no_args elim_global, Attrib.no_args elim_local),
    3.14 +    "declaration of elimination rule"),
    3.15 +  ("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local),
    3.16 +    "declaration of introduction rule"),
    3.17 +  ("delrule", (Attrib.no_args delrule_global, Attrib.no_args delrule_local),
    3.18 +    "remove declaration of elim/intro rule")];
    3.19  
    3.20  
    3.21