# HG changeset patch
# User webertj
# Date 1138112166 -3600
# Node ID 7cf74a743c32befb2dac12fd0ed105e10c89fcd7
# Parent  0eabf66582d0c3465d01671dd84c4be3887e9321
works with DPLL solver now

diff -r 0eabf66582d0 -r 7cf74a743c32 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Tue Jan 24 13:28:06 2006 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Tue Jan 24 15:16:06 2006 +0100
@@ -12,6 +12,8 @@
 
 begin
 
+refute_params [satsolver="dpll"]
+
 lemma "P \<and> Q"
   apply (rule conjI)
   refute 1  -- {* refutes @{term "P"} *}
@@ -150,7 +152,7 @@
 text {* A true statement (also testing names of free and bound variables being identical) *}
 
 lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
-  refute
+  refute [maxsize=4]
   apply fast
 done
 
@@ -1088,4 +1090,6 @@
   refute
 oops
 
+refute_params [satsolver="auto"]
+
 end