src/HOL/Isar_examples/Cantor.ML
author kleing
Sat, 01 Mar 2003 16:45:51 +0100
changeset 13840 399c8103a98f
parent 9474 b0ce3b7c9c26
permissions -rw-r--r--
keep a copy of generated files in repository


(* 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 "";


(* tactic script -- automatic *)

Goal "EX S. S ~: range (f :: 'a => 'a set)";
  by (Best_tac 1);
qed "";