src/HOL/Isar_examples/Cantor.ML
changeset 9474 b0ce3b7c9c26
parent 7578 80525697a87c
equal deleted inserted replaced
9473:7d13a5ace928 9474:b0ce3b7c9c26
     1 
     1 
     2 (* tactic script -- single steps *)
     2 (* tactic script -- single steps *)
     3 
     3 
     4 Goal "EX S. S ~: range(f :: 'a => 'a set)";
     4 Goal "EX S. S ~: range (f :: 'a => 'a set)";
     5   by (rtac exI 1);
     5   by (rtac exI 1);
     6   by (rtac notI 1);
     6   by (rtac notI 1);
     7   by (etac rangeE 1);
     7   by (etac rangeE 1);
     8   by (etac equalityCE 1);
     8   by (etac equalityCE 1);
     9   by (dtac CollectD 1);
     9   by (dtac CollectD 1);
    13 qed "";
    13 qed "";
    14 
    14 
    15 
    15 
    16 (* tactic script -- automatic *)
    16 (* tactic script -- automatic *)
    17 
    17 
    18 Goal "EX S. S ~: range(f :: 'a => 'a set)";
    18 Goal "EX S. S ~: range (f :: 'a => 'a set)";
    19   by (best_tac (claset() addSEs [equalityCE]) 1);
    19   by (Best_tac 1);
    20 qed "";
    20 qed "";