iris/bi/big_op.v · e48bc41be8a23cec99adcc6c4a25f54b598952d4 · Iris / Iris · GitLab

Find file Blame History Permalink

Rename `big_sep{L,L2,M,M2,S}_intuitionistically_forall` and `big_orL_lookup` to `big_*_intro` · e48bc41b
Ralf Jung authored May 26, 2021
```
also add `wand_entails'`, which was used in some earlier version of these proofs
```
e48bc41b