1.1 --- a/src/HOL/HOL.thy	Mon Feb 09 12:31:36 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Feb 10 14:02:45 2009 +0100
     1.3 @@ -932,7 +932,7 @@
     1.4  
     1.5  structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules");
     1.6  
     1.7 -structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "Theorems blacklisted for ATP");
     1.8 +structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "theorems blacklisted for ATP");
     1.9  *}
    1.10  
    1.11  text {*ResBlacklist holds theorems blacklisted to sledgehammer. 
    1.12 @@ -1707,17 +1707,17 @@
    1.13  structure Nitpick_Const_Simp_Thms = NamedThmsFun
    1.14  (
    1.15    val name = "nitpick_const_simp"
    1.16 -  val description = "Equational specification of constants as needed by Nitpick"
    1.17 +  val description = "equational specification of constants as needed by Nitpick"
    1.18  )
    1.19  structure Nitpick_Const_Psimp_Thms = NamedThmsFun
    1.20  (
    1.21    val name = "nitpick_const_psimp"
    1.22 -  val description = "Partial equational specification of constants as needed by Nitpick"
    1.23 +  val description = "partial equational specification of constants as needed by Nitpick"
    1.24  )
    1.25  structure Nitpick_Ind_Intro_Thms = NamedThmsFun
    1.26  (
    1.27    val name = "nitpick_ind_intro"
    1.28 -  val description = "Introduction rules for (co)inductive predicates as needed by Nitpick"
    1.29 +  val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
    1.30  )
    1.31  *}
    1.32  setup {* Nitpick_Const_Simp_Thms.setup