- Jul 23, 2022
-
-
Ralf Jung authored
-
- Jul 20, 2022
-
-
Ralf Jung authored
Remove unused Qp argument to dfrac_valid_discarded See merge request iris/iris!819
-
Tej Chajed authored
-
Ralf Jung authored
add mono_nat_lb_own_0 See merge request iris/iris!817
-
Robbert Krebbers authored
general lemma that a fixpoint is Persistent/Absorbing/Affine See merge request iris/iris!810
-
- Jul 19, 2022
-
-
Ralf Jung authored
Make saved props have discardable fractions See merge request iris/iris!802
-
-
Ralf Jung authored
-
Ralf Jung authored
Tweak priority of proof mode instances for £. Closes #470 See merge request iris/iris!818
-
Ralf Jung authored
-
Ralf Jung authored
-
-
Ralf Jung authored
-
- Jul 18, 2022
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jul 16, 2022
-
-
Robbert Krebbers authored
This closes issue #470.
-
- Jul 15, 2022
- Jul 14, 2022
-
-
Ralf Jung authored
Fupd soundness lemmas always generate credits See merge request iris/iris!815
-
-
- Jul 13, 2022
-
-
Ralf Jung authored
document wp_smart_apply See merge request iris/iris!811
-
-
Robbert Krebbers authored
-
- Jul 12, 2022
-
-
Ralf Jung authored
-
- Jul 08, 2022
-
-
Ralf Jung authored
add proofmode instances for le_upd See merge request iris/iris!813
-
Ralf Jung authored
-
- Jul 07, 2022
- Jul 05, 2022
-
-
Ralf Jung authored
First Steps for Later Credits See merge request iris/iris!792
-
-
Ralf Jung authored
-
Ralf Jung authored
not really a fully compatible replacement. we should really have an example use of this somewhere here...
-
- Jun 28, 2022
-
-
Ralf Jung authored
-
- Jun 27, 2022
