- Jan 09, 2023
-
-
Ralf Jung authored
-
- Jan 08, 2023
-
-
Ralf Jung authored
-
- Dec 08, 2022
-
-
Ralf Jung authored
Documentation about `leibnizO`. See merge request iris/iris!875
-
- Dec 07, 2022
-
-
Robbert Krebbers authored
-
- Dec 06, 2022
-
-
Robbert Krebbers authored
-
Ralf Jung authored
Rename `sig_{equiv,dist}_alt` into `sig_{equiv,dist}_def` and state using `=` instead of `<->`. See merge request iris/iris!877 -
Ralf Jung authored
Add lemma `intuitionistically_def P : □ P = <affine> <pers> P`. See merge request iris/iris!874
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
lemmas using `=` instead of `<->`.
-
- Dec 05, 2022
-
-
Ralf Jung authored
Do not write heading in readme with capitals. See merge request iris/iris!876
-
Ralf Jung authored
See discussion in https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/iris.20failing
-
Ralf Jung authored
-
Robbert Krebbers authored
-
- Dec 04, 2022
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Nov 30, 2022
- Nov 29, 2022
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
slightly generalize and reorganize fupd soundness lemmas See merge request iris/iris!863
-
-
- Nov 27, 2022
-
-
Robbert Krebbers authored
Add Fractional and AsFractional instance for embed See merge request iris/iris!868
-
- Nov 26, 2022
-
-
Simon Friis Vindum authored
-
- Nov 24, 2022
-
-
Ralf Jung authored
Add (basic) support for `gset` and `gset_disj` cameras to `set_solver`. See merge request iris/iris!871
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Remove tactic `iSolveTC` in favor of `tc_solve` in std++. See merge request iris/iris!870
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Nov 23, 2022
-
-
Ralf Jung authored
-
Ralf Jung authored
heaplang.sty: avoid clash with hyperref Closes #489 See merge request iris/iris!858
-
