# HG changeset patch
# User paulson
# Date 1091792126 -7200
# Node ID af3bca62444bf747c5a757902d776aec0010b751
# Parent  1c3be9eb41265c8aa3a31effadf019b99e6772d1
modified resolution proof

diff -r 1c3be9eb4126 -r af3bca62444b src/HOL/ex/Classical.thy
--- a/src/HOL/ex/Classical.thy	Fri Aug 06 12:30:31 2004 +0200
+++ b/src/HOL/ex/Classical.thy	Fri Aug 06 13:35:26 2004 +0200
@@ -786,16 +786,14 @@
 lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
 proof (rule ccontr, skolemize, make_clauses)
   fix f g
-  assume P: "\<And>U. P U" 
-     and Q: "\<And>U. \<not> Q U"
-     and PQ: "\<And>U. \<not> P (f U) \<or> Q (g U)"
-  from PQ [of a]
+  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"
+    by (blast intro: P PQ)
+       --{*Temporary: to be replaced by resolution attributes*}
   show False
-  proof
-    assume "\<not> P (f a)" thus False by (rule notE [OF _ P])
-  next
-    assume "Q (g a)" thus False by (rule notE [OF Q])
-  qed
+    by (blast intro: Q cl4)
 qed
 
 end