author | nipkow |
Wed, 06 Sep 2000 08:04:41 +0200 | |
changeset 9870 | 2374ba026fc6 |
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 "";