src/HOL/Isar_examples/Cantor.ML
author wenzelm
Sat Sep 04 21:13:01 1999 +0200 (1999-09-04)
changeset 7480 0a0e0dbe1269
parent 7322 d16d7ddcc842
child 7578 80525697a87c
permissions -rw-r--r--
replaced ?? by ?;
wenzelm@6516
     1
wenzelm@6516
     2
(* tactic script -- single steps *)
wenzelm@6516
     3
wenzelm@6516
     4
Goal "EX S. S ~: range(f :: 'a => 'a set)";
wenzelm@7322
     5
  by (rtac exI 1);
wenzelm@7322
     6
  by (rtac notI 1);
wenzelm@7322
     7
  by (etac rangeE 1);
wenzelm@7322
     8
  by (etac equalityCE 1);
wenzelm@7322
     9
  by (dtac CollectD 1);
wenzelm@6516
    10
  by (contr_tac 1);
wenzelm@6516
    11
  by (swap_res_tac [CollectI] 1);
wenzelm@7322
    12
  by (assume_tac 1);
wenzelm@6516
    13
qed "it";
wenzelm@6516
    14
wenzelm@6516
    15
wenzelm@6516
    16
(* tactic script -- automatic *)
wenzelm@6516
    17
wenzelm@6516
    18
Goal "EX S. S ~: range(f :: 'a => 'a set)";
wenzelm@6516
    19
  by (best_tac (claset() addSEs [equalityCE]) 1);
wenzelm@6516
    20
qed "it";