author | wenzelm |
Sat, 04 Sep 1999 21:13:01 +0200 | |
changeset 7480 | 0a0e0dbe1269 |
parent 7322 | d16d7ddcc842 |
child 7578 | 80525697a87c |
permissions | -rw-r--r-- |
6516 | 1 |
|
2 |
(* tactic script -- single steps *) |
|
3 |
||
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); |
6516 | 13 |
qed "it"; |
14 |
||
15 |
||
16 |
(* tactic script -- automatic *) |
|
17 |
||
18 |
Goal "EX S. S ~: range(f :: 'a => 'a set)"; |
|
19 |
by (best_tac (claset() addSEs [equalityCE]) 1); |
|
20 |
qed "it"; |