 11 Jul, 2017 1 commit


Ralf Jung authored

 27 Jun, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 13 Jun, 2017 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
It can be derived, thanks to Ales for noticing!

 12 Jun, 2017 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 08 Jun, 2017 7 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
when using iCombine.

 06 Jun, 2017 1 commit


Robbert Krebbers authored
TODO: document this.

 25 May, 2017 1 commit


Robbert Krebbers authored

 17 May, 2017 1 commit


Robbert Krebbers authored

 12 May, 2017 7 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
Otherwise, the tactic will fail subsequently. Besides, it was inconsistent w.r.t. the iLöb tactic, which was already doing this.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

 09 May, 2017 1 commit


Robbert Krebbers authored

 27 Apr, 2017 2 commits


Robbert Krebbers authored
Now they can also be used to clear/frame the whole pure/persistent/spatial context.

Robbert Krebbers authored

 26 Apr, 2017 1 commit


Robbert Krebbers authored
After discussing this with Ralf, again, it turned out that using a bar instead of a turnstyle would be better. When formalizing type systems, one often wants to use a turnstyle in other notations (the typing judgment), so having the turnstyle in the proofmode notation is confusing.

 19 Apr, 2017 3 commits
 13 Apr, 2017 6 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This enables things like `iSpecialize ("H2" with "H1") in the below: "H1" : P □ "H2" : □ P ∗ Q ∗ R

Robbert Krebbers authored

 12 Apr, 2017 1 commit


Ralf Jung authored
