Forked from
Iris / Iris
1972 commits behind the upstream repository.
-
Robbert Krebbers authored
It used to be: (P ={E}=> Q) := (True ⊢ (P → |={E}=> Q)) Now it is: (P ={E}=> Q) := (P ⊢ |={E}=> Q)Robbert Krebbers authoredIt used to be: (P ={E}=> Q) := (True ⊢ (P → |={E}=> Q)) Now it is: (P ={E}=> Q) := (P ⊢ |={E}=> Q)
