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 /cfrontend/SimplExpr.v | |
parent | 47e0a23aae7bed06f5ceaf4df1f95ec14101f9f1 (diff) | |
download | compcert-795485179071254bfab493dd6733d45b8f272900.tar.gz compcert-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 'cfrontend/SimplExpr.v')
0 files changed, 0 insertions, 0 deletions