Hi Gerwin,
Am 27.11.2014 um 00:06 schrieb Gerwin Klein <gerwin.kl...@nicta.com.au>:
> I wonder if it would be feasible to create a regression test for interactive
> commands like find_theorems so this noticed earlier, but that is a different
> topic.
We have regression tests for a number of other interactive diagnosis commands
-- I'm aware of "nitpick", "quickcheck", and "sledgehammer", and there might be
others. For these, it's done simply by adding an option to the command to
specify the expected result, e.g.
sledgehammer [expect = some]
(where "some" means "some proof"). Something like that could surely be done for
"find_theorems", if there's enough willpower. ;)
Cheers,
Jasmin
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
