
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
 




