[isabelle-dev] Function package produces "duplicate rewrite rule" warnings
gerwin.klein at nicta.com.au
Tue May 4 23:58:54 CEST 2010
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