 12 Jul, 2017 2 commits


Robbert Krebbers committed

Robbert Krebbers committed

 11 Jul, 2017 1 commit


Ralf Jung committed

 27 Jun, 2017 2 commits


Robbert Krebbers committed

Robbert Krebbers committed

 13 Jun, 2017 3 commits


Robbert Krebbers committed

Robbert Krebbers committed

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

 12 Jun, 2017 3 commits


Robbert Krebbers committed

Robbert Krebbers committed

Robbert Krebbers committed

 08 Jun, 2017 7 commits


Robbert Krebbers committed

Robbert Krebbers committed

Robbert Krebbers committed

Robbert Krebbers committed

Robbert Krebbers committed

Robbert Krebbers committed

when using iCombine.
Robbert Krebbers committed

 06 Jun, 2017 1 commit


 25 May, 2017 1 commit


Robbert Krebbers committed

 17 May, 2017 1 commit


Robbert Krebbers committed

 12 May, 2017 7 commits


Robbert Krebbers committed

Robbert Krebbers committed

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

Robbert Krebbers committed

Robbert Krebbers committed

Ralf Jung committed

 09 May, 2017 1 commit


Robbert Krebbers committed

 27 Apr, 2017 2 commits


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

 26 Apr, 2017 1 commit


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.
Robbert Krebbers committed

 19 Apr, 2017 3 commits
 13 Apr, 2017 5 commits


Robbert Krebbers committed

Robbert Krebbers committed

Robbert Krebbers committed

Robbert Krebbers committed

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