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

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

     3.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Aug 26 20:42:09 2010 +0200
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Aug 26 21:04:22 2010 +0200
     3.3 @@ -235,39 +235,49 @@
     3.4  
     3.5  (* equivalence relation theorems *)
     3.6  structure EquivRules = Named_Thms
     3.7 -  (val name = "quot_equiv"
     3.8 -   val description = "Equivalence relation theorems.")
     3.9 +(
    3.10 +  val name = "quot_equiv"
    3.11 +  val description = "equivalence relation theorems"
    3.12 +)
    3.13  
    3.14  val equiv_rules_get = EquivRules.get
    3.15  val equiv_rules_add = EquivRules.add
    3.16  
    3.17  (* respectfulness theorems *)
    3.18  structure RspRules = Named_Thms
    3.19 -  (val name = "quot_respect"
    3.20 -   val description = "Respectfulness theorems.")
    3.21 +(
    3.22 +  val name = "quot_respect"
    3.23 +  val description = "respectfulness theorems"
    3.24 +)
    3.25  
    3.26  val rsp_rules_get = RspRules.get
    3.27  val rsp_rules_add = RspRules.add
    3.28  
    3.29  (* preservation theorems *)
    3.30  structure PrsRules = Named_Thms
    3.31 -  (val name = "quot_preserve"
    3.32 -   val description = "Preservation theorems.")
    3.33 +(
    3.34 +  val name = "quot_preserve"
    3.35 +  val description = "preservation theorems"
    3.36 +)
    3.37  
    3.38  val prs_rules_get = PrsRules.get
    3.39  val prs_rules_add = PrsRules.add
    3.40  
    3.41  (* id simplification theorems *)
    3.42  structure IdSimps = Named_Thms
    3.43 -  (val name = "id_simps"
    3.44 -   val description = "Identity simp rules for maps.")
    3.45 +(
    3.46 +  val name = "id_simps"
    3.47 +  val description = "identity simp rules for maps"
    3.48 +)
    3.49  
    3.50  val id_simps_get = IdSimps.get
    3.51  
    3.52  (* quotient theorems *)
    3.53  structure QuotientRules = Named_Thms
    3.54 -  (val name = "quot_thm"
    3.55 -   val description = "Quotient theorems.")
    3.56 +(
    3.57 +  val name = "quot_thm"
    3.58 +  val description = "quotient theorems"
    3.59 +)
    3.60  
    3.61  val quotient_rules_get = QuotientRules.get
    3.62  val quotient_rules_add = QuotientRules.add

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