Merge requests · Iris / Iris · GitLab

move the reduction control of the proofmode to its own file and tweak it

!150 · created May 24, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 67
updated Jun 15, 2018
provide big_op lemmas outside of bi module

!149 · created May 23, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 8
updated May 29, 2018
Make uPred itself independent of BI interface and just prove primitive laws (like in master branch)

!148 · created May 23, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 48
updated Jun 05, 2018
more consistent lemma naming

!135 · created Mar 22, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 1
updated Apr 03, 2018
add notation to define the PROP we use for a particular turnstile

!134 · created Mar 21, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 44
updated Apr 05, 2018
move Frame instances to their own file

!133 · created Mar 21, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 4
updated Mar 22, 2018
rename valid -> emp_valid

!131 · created Mar 19, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 15
updated Jul 13, 2018
rename affinely_persistently -> intuitionistically; and make it a TC-opaque definition

!130 · created Mar 19, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode T-proofmode
- MERGED
- 28
updated Mar 22, 2018
Extend ElimModal with Boolean flags to specify whether it operates on the…

!129 · created Mar 15, 2018 by Robbert Krebbers Generalized Proofmode Merger gen_proofmode
- MERGED
- 11
updated Apr 05, 2018
Factor plainly out of main BI interface

!98 · created Dec 06, 2017 by Ralf Jung Generalized Proofmode Merger gen_proofmode T-proofmode
- CLOSED
- 171
updated Mar 03, 2018