equal
deleted
inserted
replaced
10 |
10 |
11 set proof_timing; |
11 set proof_timing; |
12 |
12 |
13 (*Perhaps equalities.ML shouldn't add this in the first place!*) |
13 (*Perhaps equalities.ML shouldn't add this in the first place!*) |
14 Delsimps [image_Collect]; |
14 Delsimps [image_Collect]; |
15 |
|
16 |
|
17 (*** General lemmas ***) |
|
18 |
|
19 Goal "UNIV Times UNIV = UNIV"; |
|
20 by Auto_tac; |
|
21 qed "UNIV_Times_UNIV"; |
|
22 Addsimps [UNIV_Times_UNIV]; |
|
23 |
|
24 Goal "- (UNIV Times A) = UNIV Times (-A)"; |
|
25 by Auto_tac; |
|
26 qed "Compl_Times_UNIV1"; |
|
27 |
|
28 Goal "- (A Times UNIV) = (-A) Times UNIV"; |
|
29 by Auto_tac; |
|
30 qed "Compl_Times_UNIV2"; |
|
31 |
|
32 Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; |
|
33 |
15 |
34 |
16 |
35 (*** The abstract type of programs ***) |
17 (*** The abstract type of programs ***) |
36 |
18 |
37 val rep_ss = simpset() addsimps |
19 val rep_ss = simpset() addsimps |