[isabelle-dev] Function package produces "duplicate rewrite rule" warnings
makarius at sketis.net
Wed May 5 15:25:47 CEST 2010
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.
More information about the isabelle-dev