[isabelle-dev] NEWS: Dockable window "Find"

[Makarius]

On Fri, 9 Aug 2013, Gerwin Klein wrote:

>> Is this special "Duplicates" treatment still relevant?
>
> Yes, it's still relevant. One of the uses of the command where 
> duplicates are reported is to see how often the same theorem is proved 
> under different names, which these are, and how to best consolidate 
> them. It's usually used with narrow search parameters, so that the 
> result lists tend to be small. It's less about the speed of the output 
> (that may have been a consideration very early on, but not in the last 
> years).

OK, can you rephrase this as a tooltip text?  (Following the style of the 
other tooltips.)


 	Makarius