Merge requests · Iris / Iris

Simplify cinv proofs.

!1108 · created Mar 07, 2025 by Janggun Lee
- Merged
- 5
updated Mar 11, 2025
Enable specifying which directions of AsEmpValid hold

!1104 · created Feb 08, 2025 by Michael Sammler
- Merged
- 33
updated Mar 11, 2025
reference: clarify use of quotient

!1107 · created Feb 19, 2025 by Ralf Jung
- Merged
- 1
updated Feb 19, 2025
Missing `included`/`includedN` lemmas for `excl`/`agree`, simplify `excl_includedI`

!1106 · created Feb 10, 2025 by Robbert Krebbers
- Merged
- 4
updated Feb 12, 2025
New proof `limit_preserving_entails`, remove duplicate `limit_preserving_equiv`

!1105 · created Feb 09, 2025 by Robbert Krebbers
S-waiting-for-review
- Merged
- 1
updated Feb 10, 2025
add fixpoint lemmas for BI properties

!1103 · created Feb 07, 2025 by Ralf Jung
- Merged
- 3
updated Feb 08, 2025
rename bi.lib.fixpoint → bi.lib.fixpoint_mono

!1102 · created Feb 07, 2025 by Ralf Jung
- Merged
- 2
updated Feb 07, 2025
Use gmake for BSD systems

!1061 · created Jul 31, 2024 by Yiyun Liu
- Merged
- 3
updated Feb 06, 2025
fix CsumInvalid name

!1098 · created Feb 05, 2025 by Ralf Jung
- Merged
- 1
updated Feb 05, 2025
rename CSumBot → CSumInvalid

!1096 · created Jan 31, 2025 by Ralf Jung
- Merged
- 5
updated Feb 05, 2025
WP notation: support type ascription for binder

!1095 · created Dec 13, 2024 by Ralf Jung
- Merged
- 4
- 1
updated Jan 31, 2025
Add rule `own_forall` (base logic part of !1052)

!1078 · created Sep 24, 2024 by Robbert Krebbers
- Merged
- 16
updated Dec 06, 2024
Resolve conflicts between iris.sty and acmart

!1060 · created Jul 30, 2024 by Ralf Jung
- Merged
- 5
updated Dec 04, 2024
merge two fupd_plainly laws into one

!1085 · created Oct 29, 2024 by Ralf Jung
- Merged
- 19
updated Nov 28, 2024
Add lemma `ufrac_auth_update_surplus_cancel`.

!1092 · created Nov 16, 2024 by Robbert Krebbers
- Merged
- 2
updated Nov 27, 2024
let users access iFrame helper tactics

!648 · created Mar 12, 2021 by Ralf Jung
- Merged
- 5
updated Nov 25, 2024
Add requirement of mathpartir to pftools.sty

!1087 · created Oct 31, 2024 by Isaac van Bakel
- Merged
- 1
updated Nov 15, 2024
bupd_alt.v: fix thinko in docs

!1088 · created Nov 10, 2024 by Paolo G. Giarrusso
- Merged
- 1
updated Nov 13, 2024
remove link to iris club mailing list from readme

!1091 · created Nov 13, 2024 by Ralf Jung
- Merged
updated Nov 13, 2024
Constrain lock_name to be Inhabited

!1089 · created Nov 11, 2024 by Daniel Nezamabadi
- Merged
- 2
updated Nov 13, 2024