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

[Gerwin Klein]

Hi Stefan,

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)

Cheers,
Gerwin