| changeset 6516 | 09207771cc7c |
| child 7322 | d16d7ddcc842 |
| 6515:18e113be12ee | 6516:09207771cc7c |
|---|---|
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"; |