[isabelle-dev] Bad binding warnings
noschinl at in.tum.de
Thu Jul 14 22:53:38 CEST 2011
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
fixes A :: 'a
assumes "P A"
More information about the isabelle-dev