
diff -r acbc7a9c3864 -r 19b4bf469fb2 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Mon Jul 25 21:40:43 2005 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Tue Jul 26 12:13:35 2005 +0200
@@ -150,7 +150,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 [maxsize=6]
+  refute
   apply fast
 done
 
@@ -258,7 +258,7 @@
         \<longrightarrow> trans_closure TP P
         \<longrightarrow> trans_closure TR R
         \<longrightarrow> (T x y = (TP x y | TR x y))"
-  refute [satsolver="dpll"]
+  refute
 oops
 
 text {* "Every surjective function is invertible." *}




