diff -r aa2764dda077 -r 0cf192e489e2 src/HOL/ex/Classical.thy
--- a/src/HOL/ex/Classical.thy	Thu Jan 04 17:52:28 2007 +0100
+++ b/src/HOL/ex/Classical.thy	Thu Jan 04 17:55:12 2007 +0100
@@ -825,7 +825,7 @@
 
 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)
+proof (neg_clausify)
   fix x
   assume P: "\<And>U. P U" 
      and Q: "\<And>U. ~ Q U"
@@ -844,7 +844,7 @@
 
 text{*Full single-step proof*}
 lemma "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-proof (rule ccontr, skolemize, make_clauses)
+proof (neg_clausify)
   fix S :: "'a set set"
   assume CL1: "\<And>Z. ~ (S \<subseteq> {Z})"
      and CL2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
@@ -872,7 +872,7 @@
 text{*Partially condensed proof*}
 lemma singleton_example_1:
      "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-proof (rule ccontr, skolemize, make_clauses)
+proof (neg_clausify)
   fix S :: "'a set set"
   assume CL1: "\<And>Z. ~ (S \<subseteq> {Z})"
      and CL2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
@@ -890,7 +890,7 @@
 (**Not working: needs Metis
 text{*More condensed proof*}
 lemma "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-proof (rule ccontr, skolemize, make_clauses)
+proof (neg_clausify)
   fix S :: "'a set set"
   assume CL1: "\<And>Z. ~ (S \<subseteq> {Z})"
      and CL2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"