- Jul 14, 2020
- Jul 10, 2020
-
-
Ralf Jung authoredLICENSE-CODE: Clarify which BSD license is being used See merge request iris/iris!472
-
-
- Jul 04, 2020
-
-
Ralf Jung authored
-
- Jul 03, 2020
-
-
Ralf Jung authored
-
- Jul 02, 2020
-
-
Ralf Jung authored
Mention change to lemmas in changelog See merge request iris/iris!469
-
Simon Friis Vindum authored -
Ralf Jung authored
adjust notation for step-taking updates See merge request iris/iris!462
-
Ralf Jung authored
-
- Jul 01, 2020
-
-
Robbert Krebbers authored
Add lemmas for creating big op from duplicable resource See merge request iris/iris!468
-
Robbert Krebbers authored
-
- Jun 30, 2020
-
-
Simon Friis Vindum authored
-
- Jun 29, 2020
-
-
Simon Friis Vindum authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Simon Friis Vindum authored
-
- Jun 26, 2020
- Jun 19, 2020
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
Port to Coq #12512. See merge request iris/iris!465
-
Robbert Krebbers authored
-
- Jun 18, 2020
-
-
Ralf Jung authored
-
-
Ralf Jung authored
-
Robbert Krebbers authored
Add natural numbers with min RA Closes #324 See merge request !461
-
Simon Friis Vindum authored
-
Ralf Jung authored
-
- Jun 17, 2020
-
-
Ralf Jung authored
-
Simon Friis Vindum authored
-
Simon Friis Vindum authored
Add IdempP instances for min_nat and max_nat. Move additional numbers related lemmas and instances into the numbers file.
-
- Jun 16, 2020
-
-
Simon Friis Vindum authored
-
- Jun 15, 2020
-
-
Robbert Krebbers authored
Use [fill K] in tac_wp_pure See merge request iris/iris!463
-
Tej Chajed authored
This is more consistent with other tac_wp tactics for HeapLang and also a tiny bit more efficient, which is good to embody in the basic tactics so derived code follows the same patterns.
-
- Jun 13, 2020
-
-
Simon Friis Vindum authored
-
