On 14.07.2011 21:20, Makarius wrote:
Recently I've noticed that internal "fixes" where accidentally omitted from the binding check. There were also some incidents and genuine programming errors introduced due to the absence of a proper check.
Is it to be expected, that this warning now occurs quite often in a lemma statement, even if Auto Quickcheck and Solve are disabled? E.g. the following theory triggers it, but only in interactive mode:
-------------- theory Scratch imports Plain begin lemma fixes A :: 'a assumes "P A" shows "Q" oops end --------------- -- Lars _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
