# HG changeset patch
# User blanchet
# Date 1234270965 -3600
# Node ID a7a8b90cd882305de7edf2dadc3a54a37b441578
# Parent  787349bb53e9309a1ec03b83062f990eeca186e2
Renamed descriptions of Nitpick (and ATP) attributes, so that they fit well with the rest of the sentence in ProofGeneral.

diff -r 787349bb53e9 -r a7a8b90cd882 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Feb 09 12:31:36 2009 +0100
+++ b/src/HOL/HOL.thy	Tue Feb 10 14:02:45 2009 +0100
@@ -932,7 +932,7 @@
 
 structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules");
 
-structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "Theorems blacklisted for ATP");
+structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "theorems blacklisted for ATP");
 *}
 
 text {*ResBlacklist holds theorems blacklisted to sledgehammer. 
@@ -1707,17 +1707,17 @@
 structure Nitpick_Const_Simp_Thms = NamedThmsFun
 (
   val name = "nitpick_const_simp"
-  val description = "Equational specification of constants as needed by Nitpick"
+  val description = "equational specification of constants as needed by Nitpick"
 )
 structure Nitpick_Const_Psimp_Thms = NamedThmsFun
 (
   val name = "nitpick_const_psimp"
-  val description = "Partial equational specification of constants as needed by Nitpick"
+  val description = "partial equational specification of constants as needed by Nitpick"
 )
 structure Nitpick_Ind_Intro_Thms = NamedThmsFun
 (
   val name = "nitpick_ind_intro"
-  val description = "Introduction rules for (co)inductive predicates as needed by Nitpick"
+  val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
 )
 *}
 setup {* Nitpick_Const_Simp_Thms.setup