[isabelle-dev] counter example checking from ML

Lucas Dixon ldixon at inf.ed.ac.uk
Fri Sep 25 23:35:20 CEST 2009

Thanks, this explains why the behaviour changed, but I think it would
still be better to avoid checking the same counter-example more than
once? We certainly need this, and more generally this will improve
counter-example finding.

I'll also have a go at using your new in-development stuff to
deterministically generate counter-examples - but that will take me a
week to get to as I have other priorities right now.

All the best,

Florian Haftmann wrote:
> Hi Lucas,
> perhaps the source of the confusion can be found here:
> http://isabelle.in.tum.de/repos/isabelle/file/6b31b143f18b/src/Pure/codegen.ML
> I.e. due to a misunderstanding of interfacing convention (0 is also a
> valid size), Codegn.test_term in Isabelle2009 would increase its size
> argument by 1, which should not happen.
> Hope this helps,
> 	Florian

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

More information about the isabelle-dev mailing list