# HG changeset patch
# User webertj
# Date 1122372815 -7200
# Node ID 19b4bf469fb26264ad1adb23ac7a70010bf20748
# Parent  acbc7a9c3864698463a6111d7f1ebb2ce9f11790
minor parameter changes

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." *}