equal
deleted
inserted
replaced
1 |
1 |
2 (* tactic script -- single steps *) |
2 (* tactic script -- single steps *) |
3 |
3 |
4 Goal "EX S. S ~: range(f :: 'a => 'a set)"; |
4 Goal "EX S. S ~: range (f :: 'a => 'a set)"; |
5 by (rtac exI 1); |
5 by (rtac exI 1); |
6 by (rtac notI 1); |
6 by (rtac notI 1); |
7 by (etac rangeE 1); |
7 by (etac rangeE 1); |
8 by (etac equalityCE 1); |
8 by (etac equalityCE 1); |
9 by (dtac CollectD 1); |
9 by (dtac CollectD 1); |
13 qed ""; |
13 qed ""; |
14 |
14 |
15 |
15 |
16 (* tactic script -- automatic *) |
16 (* tactic script -- automatic *) |
17 |
17 |
18 Goal "EX S. S ~: range(f :: 'a => 'a set)"; |
18 Goal "EX S. S ~: range (f :: 'a => 'a set)"; |
19 by (best_tac (claset() addSEs [equalityCE]) 1); |
19 by (Best_tac 1); |
20 qed ""; |
20 qed ""; |