Skip to content
Snippets Groups Projects
Select Git revision
  • polymorphic-bi
  • master default protected
  • fix-doc-links
  • parametric-algebra
  • fix-proof-coq-master
  • dfrac-valid-arg
  • avoid-deprecated-arith
  • adjust-focused-goal
  • prefix-automatic-names
  • qualify-instances
  • exists-intro-pattern
  • document-ipm-classes
  • fix-intuitionistic-spatial
  • strong-frag-validity/view-bij
  • dfrac-smart-constructor
  • rauth
  • cmra-restrict-valid
  • cmra-iso
  • port-auth_map
  • efficient-heaplang-tactics
  • iris-3.1.0
  • iris-3.0.0
  • iris-2.0
  • iris-2.0-rc2
  • iris-2.0-rc1
  • iris-1.1
  • iris-1.0
  • hope-2015-coq-1
  • appendix-1.0.0
  • appendix-1
30 results
Compare
Forked from Iris / Iris
Source project has a limited visibility.
user avatar
Prove some lemmas about uPred that I am used to
Ralf Jung authored 
I planned to use them to simplify wsat_le, but it did not turn out to be simpler.
951d8927
History
user avatar 951d8927
History
Name Last commit Last update