author | kleing |
Sat, 01 Mar 2003 16:45:51 +0100 | |
changeset 13840 | 399c8103a98f |
parent 9474 | b0ce3b7c9c26 |
permissions | -rw-r--r-- |
(* 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 "";