[isabelle-dev] NEWS: Dockable window "Find"
makarius at sketis.net
Fri Aug 9 21:17:57 CEST 2013
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
OK, can you rephrase this as a tooltip text? (Following the style of the
More information about the isabelle-dev