Merge requests · Iris / Iris · GitLab

Add stuckness bits to WP.

!80 · created Nov 09, 2017 by David Swasey Iris 3.1
- MERGED
- 79
updated Feb 02, 2018
Prove that uPred is complete even if we remove the validity restriction in uPred_closed.

!99 · created Dec 06, 2017 by Jacques-Henri Jourdan Iris 3.1
- MERGED
- 21
updated Dec 08, 2017
Get rid of `ofe_fun`, it was just a non-dependently typed version of `iprod`

!88 · created Nov 21, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 34
updated Nov 28, 2017
do not make use of wp_bind_inv unnecessarily

!87 · created Nov 21, 2017 by Ralf Jung Iris 3.1
- MERGED
- 16
updated Nov 24, 2017
Use solely canonical structures for language hierarchy.

!90 · created Nov 23, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 12
updated Nov 24, 2017
saved predicates: use ofe_fun, not ofe_mor

!86 · created Nov 21, 2017 by Ralf Jung Iris 3.1
- MERGED
- 9
updated Nov 22, 2017
generalize savedProp to let the user control the position of the type-level later

!76 · created Oct 29, 2017 by Ralf Jung Iris 3.1
- MERGED
- 45
updated Nov 18, 2017
Improved treatment of anonymous hypotheses in the proof mode

!83 · created Nov 11, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 6
updated Nov 16, 2017
add later_ne; make later_proper match the other _proper lemmas

!81 · created Nov 11, 2017 by Ralf Jung Iris 3.1
- MERGED
- 8
updated Nov 11, 2017
Get rid of `later_proper'`

!82 · created Nov 11, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 1
updated Nov 11, 2017
Add progress bit to WP.

!37 · created Dec 17, 2016 by David Swasey Iris 3.1
- MERGED
- 68
updated Nov 09, 2017
rename sub_values -> sub_redexes_are_values

!79 · created Nov 04, 2017 by Ralf Jung Iris 3.1
- MERGED
- 7
updated Nov 07, 2017
add a strong form of atomicity, for weak forms of weakest-pre

!77 · created Oct 29, 2017 by Ralf Jung Iris 3.1
- MERGED
- 22
updated Nov 05, 2017
Make proofnode notation more robust in the context of import order

!75 · created Oct 29, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 13
updated Nov 05, 2017
Rules for fancy updates and plain propositions.

!74 · created Oct 27, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 5
updated Oct 29, 2017
The plainness modality

!71 · created Oct 18, 2017 by Amin Timany Iris 3.1
- MERGED
- 91
updated Oct 29, 2017
Notation for disjointness: replace ⊥ with ##, so that ⊥ can be used for bottom.

!73 · created Oct 27, 2017 by Jacques-Henri Jourdan Iris 3.1
- MERGED
- 1
updated Oct 29, 2017