# HG changeset patch
# User wenzelm
# Date 964954976 -7200
# Node ID b0ce3b7c9c26f6e943732ed2c47cf5efd41521d2
# Parent  7d13a5ace928ed04e98970c8707f6f0917cf6dd5
removed equalityCE;

diff -r 7d13a5ace928 -r b0ce3b7c9c26 src/HOL/Isar_examples/Cantor.ML
--- a/src/HOL/Isar_examples/Cantor.ML	Sun Jul 30 13:02:14 2000 +0200
+++ b/src/HOL/Isar_examples/Cantor.ML	Sun Jul 30 13:02:56 2000 +0200
@@ -1,7 +1,7 @@
 
 (* tactic script -- single steps *)
 
-Goal "EX S. S ~: range(f :: 'a => 'a set)";
+Goal "EX S. S ~: range (f :: 'a => 'a set)";
   by (rtac exI 1);
   by (rtac notI 1);
   by (etac rangeE 1);
@@ -15,6 +15,6 @@
 
 (* tactic script -- automatic *)
 
-Goal "EX S. S ~: range(f :: 'a => 'a set)";
-  by (best_tac (claset() addSEs [equalityCE]) 1);
+Goal "EX S. S ~: range (f :: 'a => 'a set)";
+  by (Best_tac 1);
 qed "";
diff -r 7d13a5ace928 -r b0ce3b7c9c26 src/HOL/Isar_examples/Cantor.thy
--- a/src/HOL/Isar_examples/Cantor.thy	Sun Jul 30 13:02:14 2000 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Sun Jul 30 13:02:56 2000 +0200
@@ -95,16 +95,15 @@
 
 text {*
  How much creativity is required?  As it happens, Isabelle can prove
- this theorem automatically.  The context of Isabelle's classical
- prover contains rules for most of the constructs of HOL's set theory.
- We must augment it with \name{equalityCE} to break up set equalities,
- and then apply best-first search.  Depth-first search would diverge,
- but best-first search successfully navigates through the large search
- space.
+ this theorem automatically using best-first search.  Depth-first
+ search would diverge, but best-first search successfully navigates
+ through the large search space.  The context of Isabelle's classical
+ prover contains rules for the relevant constructs of HOL's set
+ theory.
 *};
 
 theorem "EX S. S ~: range (f :: 'a => 'a set)";
-  by (best elim: equalityCE);
+  by best;
 
 text {*
  While this establishes the same theorem internally, we do not get any