src/HOL/Isar_examples/Cantor.ML
changeset 9474 b0ce3b7c9c26
parent 7578 80525697a87c
     1.1 --- a/src/HOL/Isar_examples/Cantor.ML	Sun Jul 30 13:02:14 2000 +0200
     1.2 +++ b/src/HOL/Isar_examples/Cantor.ML	Sun Jul 30 13:02:56 2000 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  
     1.5  (* tactic script -- single steps *)
     1.6  
     1.7 -Goal "EX S. S ~: range(f :: 'a => 'a set)";
     1.8 +Goal "EX S. S ~: range (f :: 'a => 'a set)";
     1.9    by (rtac exI 1);
    1.10    by (rtac notI 1);
    1.11    by (etac rangeE 1);
    1.12 @@ -15,6 +15,6 @@
    1.13  
    1.14  (* tactic script -- automatic *)
    1.15  
    1.16 -Goal "EX S. S ~: range(f :: 'a => 'a set)";
    1.17 -  by (best_tac (claset() addSEs [equalityCE]) 1);
    1.18 +Goal "EX S. S ~: range (f :: 'a => 'a set)";
    1.19 +  by (Best_tac 1);
    1.20  qed "";