[isabelle-dev] Abbreviations and find_theorems
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Thu Nov 27 00:52:30 CET 2014
Am 27.11.2014 um 00:06 schrieb Gerwin Klein <gerwin.klein at 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. ;)
More information about the isabelle-dev