Skip to content

restructure I/IW instantiation files

Sergey Bozhko requested to merge sbozhko/rt-proofs:restructure-iw into master

There are a lot of lemmas inside of [abstract/ideal/iw_instantiation.v] that are not specific to ideal uni-processor. This MR moves such lemmas to [abstract/iw_auxiliary.v]

Merge request reports