# HG changeset patch
# User paulson
# Date 1134573281 -3600
# Node ID b1eab0eb7fec101c327d63662eb76753675d81be
# Parent  afb1a52a7011e0472270413a5d5db60fd87d00ed
modified example for new clauses

diff -r afb1a52a7011 -r b1eab0eb7fec src/HOL/ex/Classical.thy
--- a/src/HOL/ex/Classical.thy	Wed Dec 14 16:14:26 2005 +0100
+++ b/src/HOL/ex/Classical.thy	Wed Dec 14 16:14:41 2005 +0100
@@ -823,11 +823,11 @@
 text{*A manual resolution proof of problem 19.*}
 lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
 proof (rule ccontr, skolemize, make_clauses)
-  fix f g
+  fix x
   assume P: "\<And>U. \<not> P U \<Longrightarrow> False" 
      and Q: "\<And>U. Q U \<Longrightarrow> False"
-     and PQ: "\<And>U.  \<lbrakk>P (f U); \<not> Q (g U)\<rbrakk> \<Longrightarrow> False"
-  have cl4: "\<And>U. \<not> Q (g U) \<Longrightarrow> False"
+     and PQ: "\<lbrakk>P x; \<not> Q x\<rbrakk> \<Longrightarrow> False"
+  have cl4: "\<And>U. \<not> Q x \<Longrightarrow> False"
     by (rule P [binary 0 PQ 0])
   show "False"
     by (rule Q [binary 0 cl4 0])