Skip to content
  • Ralf Jung's avatar
    strengthen auth and heap rules to only require the assertion under a later · e9c6a8ea
    Ralf Jung authored
    Whenever clients get this stuff out of invariants, this is much more convenient for them, compared to applying timelessness themselves.
    On the other hand, this makes the test proofs slightly more annoying, since they have to manually strip away that later. I am not sure if it is worth having separate lemmas (well, tactics, soon) for that.
    Eventually, we should have a tactic which, given "... * P * ... |- ... * \later^n P * ...", automatically gets rid of the P.