[isabelle-dev] Function package produces "duplicate rewrite rule" warnings

[Makarius]

On Wed, 5 May 2010, Gerwin Klein wrote:

> On 04/05/2010, at 11:18 PM, Stefan Berghofer wrote:
>> I introduced this
>> problem when adding new infrastructure for the pre-simplification of
>> goals produced by the induct and cases methods.
>
> This sounds cool! I hope it is optional, though?
>
> I'm fearing lots of update trouble.. (at the same time looking forward 
> to using it in new proofs)

There is a "no_simp" option for the induct method.  You have to guess this 
from the sources, because there is still no NEWS entry for this, just like 
for many other things from the past few months.


 	Makarius