src/HOL/Isar_examples/Cantor.ML
author wenzelm
Mon, 23 Aug 1999 15:30:26 +0200
changeset 7322 d16d7ddcc842
parent 6516 09207771cc7c
child 7578 80525697a87c
permissions -rw-r--r--
isatool expandshort;


(* tactic script -- single steps *)

Goal "EX S. S ~: range(f :: 'a => 'a set)";
  by (rtac exI 1);
  by (rtac notI 1);
  by (etac rangeE 1);
  by (etac equalityCE 1);
  by (dtac CollectD 1);
  by (contr_tac 1);
  by (swap_res_tac [CollectI] 1);
  by (assume_tac 1);
qed "it";


(* tactic script -- automatic *)

Goal "EX S. S ~: range(f :: 'a => 'a set)";
  by (best_tac (claset() addSEs [equalityCE]) 1);
qed "it";