# HG changeset patch
# User wenzelm
# Date 968352667 -7200
# Node ID 93d2fde0306c9fb0911df5dc8186e140866b6c19
# Parent  be0389a64ce800386aacaada3a7c0a0ac7677e41
tuned msg;

diff -r be0389a64ce8 -r 93d2fde0306c src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Thu Sep 07 20:50:33 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML	Thu Sep 07 20:51:07 2000 +0200
@@ -453,8 +453,8 @@
 val setup =
   [GlobalInduct.init, LocalInduct.init,
    Attrib.add_attributes
-    [(casesN, cases_attr, "cases rule for type or set"),
-     (inductN, induct_attr, "induction rule for type or set")],
+    [(casesN, cases_attr, "declaration of cases rule for type or set"),
+     (inductN, induct_attr, "declaration of induction rule for type or set")],
    Method.add_methods
     [("cases", cases_meth oo cases_args, "case analysis on types or sets"),
      ("induct", induct_meth oo induct_args, "induction on types or sets")],
diff -r be0389a64ce8 -r 93d2fde0306c src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Sep 07 20:50:33 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Sep 07 20:51:07 2000 +0200
@@ -836,7 +836,7 @@
  [InductiveData.init,
   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
     "dynamic case analysis on sets")],
-  Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]];
+  Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
 
 
 (* outer syntax *)
diff -r be0389a64ce8 -r 93d2fde0306c src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Thu Sep 07 20:50:33 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Thu Sep 07 20:51:07 2000 +0200
@@ -305,9 +305,9 @@
 val setup =
  [GlobalRecdefData.init, LocalRecdefData.init,
   Attrib.add_attributes
-   [("recdef_simp", simp_attr, "declare recdef simp rule"),
-    ("recdef_cong", cong_attr, "declare recdef cong rule"),
-    ("recdef_wf", wf_attr, "declare recdef wf rule")]];
+   [("recdef_simp", simp_attr, "declaration of recdef simp rule"),
+    ("recdef_cong", cong_attr, "declaration of recdef cong rule"),
+    ("recdef_wf", wf_attr, "declaration of recdef wf rule")]];
 
 
 (* outer syntax *)
diff -r be0389a64ce8 -r 93d2fde0306c src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Thu Sep 07 20:50:33 2000 +0200
+++ b/src/HOL/arith_data.ML	Thu Sep 07 20:51:07 2000 +0200
@@ -426,4 +426,4 @@
     "decide linear arithmethic")],
   Attrib.add_attributes [("arith_split",
     (Attrib.no_args arith_split_add, Attrib.no_args Attrib.undef_local_attribute),
-    "declare split rules for arithmetic procedure")]];
+    "declaration of split rules for arithmetic procedure")]];
diff -r be0389a64ce8 -r 93d2fde0306c src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Thu Sep 07 20:50:33 2000 +0200
+++ b/src/Provers/clasimp.ML	Thu Sep 07 20:51:07 2000 +0200
@@ -308,7 +308,7 @@
 
 val setup =
  [Attrib.add_attributes
-  [("iff", iff_attr, "declare simplifier / classical rules")],
+  [("iff", iff_attr, "declaration of Simplifier / Classical rules")],
   Method.add_methods
    [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
     ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
diff -r be0389a64ce8 -r 93d2fde0306c src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Thu Sep 07 20:50:33 2000 +0200
+++ b/src/Provers/hypsubst.ML	Thu Sep 07 20:51:07 2000 +0200
@@ -276,6 +276,6 @@
   [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
    ("subst", subst_meth, "substitution")],
   Attrib.add_attributes
-  [("symmetric", (gen_symmetric, gen_symmetric), "apply symmetry of == or =")]];
+  [("symmetric", (gen_symmetric, gen_symmetric), "resolution with symmetry of == or =")]];
 
 end;