[isabelle-dev] counter example checking from ML
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
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:
> 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,
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
More information about the isabelle-dev