The datatype package produces some extra warning messages now too: ### Ignoring duplicate rewrite rule: ### True == induct_true
### Ignoring duplicate rewrite rule: ### False == induct_false I haven't checked, but I would be willing to bet that this behavior was introduced by the same changeset as the function package warning messages. I wouldn't be surprised if warnings pop up in other packages as well. - Brian On Mon, May 3, 2010 at 12:48 PM, Alexander Krauss <[email protected]> wrote: > Hi Brian, > > Thanks for bisecting this, I'll have a look. > > Alex > > Brian Huffman wrote: >> >> Recent versions of the function package produce some unhelpful warning >> messages about duplicate rewrite rules: >> >> ### Ignoring duplicate rewrite rule: >> ### Sum_Type.Projl (Inl ?y) == ?y >> >> ### Ignoring duplicate rewrite rule: >> ### Sum_Type.Projr (Inr ?y) == ?y _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
