author | wenzelm |
Tue, 27 Apr 1999 10:45:20 +0200 | |
changeset 6516 | 09207771cc7c |
child 7322 | d16d7ddcc842 |
permissions | -rw-r--r-- |
6516 | 1 |
|
2 |
(* tactic script -- single steps *) |
|
3 |
||
4 |
Goal "EX S. S ~: range(f :: 'a => 'a set)"; |
|
5 |
br exI 1; |
|
6 |
br notI 1; |
|
7 |
be rangeE 1; |
|
8 |
be equalityCE 1; |
|
9 |
bd CollectD 1; |
|
10 |
by (contr_tac 1); |
|
11 |
by (swap_res_tac [CollectI] 1); |
|
12 |
ba 1; |
|
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"; |