src/HOL/Isar_examples/Cantor.ML
changeset 7322 d16d7ddcc842
parent 6516 09207771cc7c
child 7578 80525697a87c
     1.1 --- a/src/HOL/Isar_examples/Cantor.ML	Mon Aug 23 15:27:27 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/Cantor.ML	Mon Aug 23 15:30:26 1999 +0200
     1.3 @@ -2,14 +2,14 @@
     1.4  (* tactic script -- single steps *)
     1.5  
     1.6  Goal "EX S. S ~: range(f :: 'a => 'a set)";
     1.7 -  br exI 1;
     1.8 -  br notI 1;
     1.9 -  be rangeE 1;
    1.10 -  be equalityCE 1;
    1.11 -  bd CollectD 1;
    1.12 +  by (rtac exI 1);
    1.13 +  by (rtac notI 1);
    1.14 +  by (etac rangeE 1);
    1.15 +  by (etac equalityCE 1);
    1.16 +  by (dtac CollectD 1);
    1.17    by (contr_tac 1);
    1.18    by (swap_res_tac [CollectI] 1);
    1.19 -  ba 1;
    1.20 +  by (assume_tac 1);
    1.21  qed "it";
    1.22  
    1.23