src/HOL/Isar_examples/Cantor.ML
author wenzelm
Tue Apr 27 10:45:20 1999 +0200 (1999-04-27)
changeset 6516 09207771cc7c
child 7322 d16d7ddcc842
permissions -rw-r--r--
added Isar_examples/Cantor.ML;
     1 
     2 (* tactic script -- single steps *)
     3 
     4 Goal "EX S. S ~: range(f :: 'a => 'a set)";
     5   br exI 1;
     6   br notI 1;
     7   be rangeE 1;
     8   be equalityCE 1;
     9   bd CollectD 1;
    10   by (contr_tac 1);
    11   by (swap_res_tac [CollectI] 1);
    12   ba 1;
    13 qed "it";
    14 
    15 
    16 (* tactic script -- automatic *)
    17 
    18 Goal "EX S. S ~: range(f :: 'a => 'a set)";
    19   by (best_tac (claset() addSEs [equalityCE]) 1);
    20 qed "it";