diff -r 52e5bf245b2a -r 691da43fbdd4 src/HOL/ex/Refute_Examples.thy --- a/src/HOL/ex/Refute_Examples.thy Sat May 03 23:15:00 2014 +0200 +++ b/src/HOL/ex/Refute_Examples.thy Sun May 04 16:17:53 2014 +0200 @@ -20,7 +20,7 @@ refute [expect = genuine] -- {* equivalent to 'refute 1' *} -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *} refute [maxsize = 5, expect = genuine] -- {* we can override parameters ... *} -refute [satsolver = "dpll", expect = genuine] 2 +refute [satsolver = "dpll_p", expect = genuine] 2 -- {* ... and specify a subgoal at the same time *} oops