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

Gerwin Klein gerwin.klein at nicta.com.au
Tue May 4 23:58:54 CEST 2010

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)


More information about the isabelle-dev mailing list