diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-09-24 11:55:10 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-09-24 11:55:10 +0200 |
| commit | 795485179071254bfab493dd6733d45b8f272900 (patch) | |
| tree | d2e0245e5f6579ff49c55cda6e8900deead2f086 /exportclight/ExportClight.ml | |
| parent | 47e0a23aae7bed06f5ceaf4df1f95ec14101f9f1 (diff) | |
| download | compcert-kvx-795485179071254bfab493dd6733d45b8f272900.tar.gz compcert-kvx-795485179071254bfab493dd6733d45b8f272900.zip | |
Add theorem "elements_remove".
Use "elements_remove" to simplify the proof of "cardinal_remove".
Simplify some of the proofs over function "xelements".
Diffstat (limited to 'exportclight/ExportClight.ml')
0 files changed, 0 insertions, 0 deletions