more uniform descriptions, which end up in the collective output of 'print_attributes' for example;

--- a/src/HOL/Tools/Function/function_common.ML	Thu Aug 26 20:42:09 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Thu Aug 26 21:04:22 2010 +0200
@@ -164,7 +164,7 @@
 structure Termination_Simps = Named_Thms
 (
   val name = "termination_simp"
-  val description = "Simplification rule for termination proofs"
+  val description = "simplification rules for termination proofs"
 )
 
 

--- a/src/HOL/Tools/Function/measure_functions.ML	Thu Aug 26 20:42:09 2010 +0200
+++ b/src/HOL/Tools/Function/measure_functions.ML	Thu Aug 26 21:04:22 2010 +0200
@@ -20,7 +20,7 @@
 (
   val name = "measure_function"
   val description =
-    "Rules that guide the heuristic generation of measure functions"
+    "rules that guide the heuristic generation of measure functions"
 );
 
 fun mk_is_measure t =

--- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Aug 26 20:42:09 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Aug 26 21:04:22 2010 +0200
@@ -235,39 +235,49 @@
 
 (* equivalence relation theorems *)
 structure EquivRules = Named_Thms
-  (val name = "quot_equiv"
-   val description = "Equivalence relation theorems.")
+(
+  val name = "quot_equiv"
+  val description = "equivalence relation theorems"
+)
 
 val equiv_rules_get = EquivRules.get
 val equiv_rules_add = EquivRules.add
 
 (* respectfulness theorems *)
 structure RspRules = Named_Thms
-  (val name = "quot_respect"
-   val description = "Respectfulness theorems.")
+(
+  val name = "quot_respect"
+  val description = "respectfulness theorems"
+)
 
 val rsp_rules_get = RspRules.get
 val rsp_rules_add = RspRules.add
 
 (* preservation theorems *)
 structure PrsRules = Named_Thms
-  (val name = "quot_preserve"
-   val description = "Preservation theorems.")
+(
+  val name = "quot_preserve"
+  val description = "preservation theorems"
+)
 
 val prs_rules_get = PrsRules.get
 val prs_rules_add = PrsRules.add
 
 (* id simplification theorems *)
 structure IdSimps = Named_Thms
-  (val name = "id_simps"
-   val description = "Identity simp rules for maps.")
+(
+  val name = "id_simps"
+  val description = "identity simp rules for maps"
+)
 
 val id_simps_get = IdSimps.get
 
 (* quotient theorems *)
 structure QuotientRules = Named_Thms
-  (val name = "quot_thm"
-   val description = "Quotient theorems.")
+(
+  val name = "quot_thm"
+  val description = "quotient theorems"
+)
 
 val quotient_rules_get = QuotientRules.get
 val quotient_rules_add = QuotientRules.add

--- a/src/HOL/ex/Numeral.thy	Thu Aug 26 20:42:09 2010 +0200
+++ b/src/HOL/ex/Numeral.thy	Thu Aug 26 21:04:22 2010 +0200
@@ -97,7 +97,7 @@
 structure Dig_Simps = Named_Thms
 (
   val name = "numeral"
-  val description = "Simplification rules for numerals"
+  val description = "simplification rules for numerals"
 )
 *}