equal
deleted
inserted
replaced
18 refute [expect = genuine] 1 -- {* refutes @{term "P"} *} |
18 refute [expect = genuine] 1 -- {* refutes @{term "P"} *} |
19 refute [expect = genuine] 2 -- {* refutes @{term "Q"} *} |
19 refute [expect = genuine] 2 -- {* refutes @{term "Q"} *} |
20 refute [expect = genuine] -- {* equivalent to 'refute 1' *} |
20 refute [expect = genuine] -- {* equivalent to 'refute 1' *} |
21 -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *} |
21 -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *} |
22 refute [maxsize = 5, expect = genuine] -- {* we can override parameters ... *} |
22 refute [maxsize = 5, expect = genuine] -- {* we can override parameters ... *} |
23 refute [satsolver = "dpll", expect = genuine] 2 |
23 refute [satsolver = "dpll_p", expect = genuine] 2 |
24 -- {* ... and specify a subgoal at the same time *} |
24 -- {* ... and specify a subgoal at the same time *} |
25 oops |
25 oops |
26 |
26 |
27 (*****************************************************************************) |
27 (*****************************************************************************) |
28 |
28 |