| changeset 7516 | a1d476251238 |
| parent 7031 | 972b5f62f476 |
| child 7823 | 742715638a01 |
| 7515:0c05469cad57 | 7516:a1d476251238 |
|---|---|
40 AddIs [vimageI]; |
40 AddIs [vimageI]; |
41 AddSEs [vimageE]; |
41 AddSEs [vimageE]; |
42 |
42 |
43 |
43 |
44 (*** Simple equalities ***) |
44 (*** Simple equalities ***) |
45 |
|
46 Goal "(%x. x) -`` B = B"; |
|
47 by (Blast_tac 1); |
|
48 qed "ident_vimage"; |
|
49 Addsimps [ident_vimage]; |
|
50 |
45 |
51 Goal "f-``{} = {}"; |
46 Goal "f-``{} = {}"; |
52 by (Blast_tac 1); |
47 by (Blast_tac 1); |
53 qed "vimage_empty"; |
48 qed "vimage_empty"; |
54 |
49 |