[isabelle-dev] Abbreviations and find_theorems

[Jasmin Christian Blanchette]

Hi Gerwin,

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. ;)

Cheers,

Jasmin