author | kleing |
Sun, 06 Apr 2003 21:16:50 +0200 | |
changeset 13901 | af38553e61ee |
parent 9474 | b0ce3b7c9c26 |
permissions | -rw-r--r-- |
6516 | 1 |
|
2 |
(* tactic script -- single steps *) |
|
3 |
||
9474 | 4 |
Goal "EX S. S ~: range (f :: 'a => 'a set)"; |
7322 | 5 |
by (rtac exI 1); |
6 |
by (rtac notI 1); |
|
7 |
by (etac rangeE 1); |
|
8 |
by (etac equalityCE 1); |
|
9 |
by (dtac CollectD 1); |
|
6516 | 10 |
by (contr_tac 1); |
11 |
by (swap_res_tac [CollectI] 1); |
|
7322 | 12 |
by (assume_tac 1); |
7578 | 13 |
qed ""; |
6516 | 14 |
|
15 |
||
16 |
(* tactic script -- automatic *) |
|
17 |
||
9474 | 18 |
Goal "EX S. S ~: range (f :: 'a => 'a set)"; |
19 |
by (Best_tac 1); |
|
7578 | 20 |
qed ""; |