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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
