theories/bi/monpred.v · 6c6d0d65b32d0d9c943031e9fa709c6c833d7ed1 · Lennard Gäher / Iris · GitLab

Find file Blame History Permalink

Weaken BI axiom `P ⊢ <pers> emp` into `emp ⊢ <pers> emp`. · 6c6d0d65
Robbert Krebbers authored Mar 16, 2018
```
The old one is admissable.

Thanks to @jtassaro and @jung.
```
6c6d0d65