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 "";