[isabelle-dev] counter example checking from ML

[Lucas Dixon]

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,
lucas

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.