-
- Downloads
Merge branch 'ralf/frac-valid' into 'master'
use Qp inequality instead of frac validity for lemma statements See merge request iris/iris!558
No related branches found
No related tags found
Showing
- CHANGELOG.md 3 additions, 0 deletionsCHANGELOG.md
- theories/algebra/auth.v 11 additions, 11 deletionstheories/algebra/auth.v
- theories/algebra/lib/frac_agree.v 3 additions, 3 deletionstheories/algebra/lib/frac_agree.v
- theories/algebra/lib/frac_auth.v 4 additions, 4 deletionstheories/algebra/lib/frac_auth.v
- theories/algebra/lib/gmap_view.v 4 additions, 4 deletionstheories/algebra/lib/gmap_view.v
- theories/algebra/lib/mnat_auth.v 3 additions, 3 deletionstheories/algebra/lib/mnat_auth.v
- theories/algebra/lib/ufrac_auth.v 1 addition, 1 deletiontheories/algebra/lib/ufrac_auth.v
- theories/algebra/view.v 12 additions, 15 deletionstheories/algebra/view.v
- theories/base_logic/algebra.v 38 additions, 31 deletionstheories/base_logic/algebra.v
- theories/base_logic/derived.v 1 addition, 0 deletionstheories/base_logic/derived.v
- theories/base_logic/lib/cancelable_invariants.v 2 additions, 2 deletionstheories/base_logic/lib/cancelable_invariants.v
- theories/base_logic/lib/gen_heap.v 3 additions, 3 deletionstheories/base_logic/lib/gen_heap.v
- theories/base_logic/lib/ghost_var.v 1 addition, 1 deletiontheories/base_logic/lib/ghost_var.v
- theories/base_logic/lib/mnat.v 2 additions, 2 deletionstheories/base_logic/lib/mnat.v
- theories/heap_lang/primitive_laws.v 4 additions, 5 deletionstheories/heap_lang/primitive_laws.v
Loading
Please register or sign in to comment