--- 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