author | wenzelm |
Sun, 30 Jul 2000 13:02:56 +0200 | |
changeset 9474 | b0ce3b7c9c26 |
parent 7578 | 80525697a87c |
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 "";