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