Also, higher cost for [elim_modal_bupd_fupd], so that it is not taken in place of [elim_modal_fupd_fupd] in spec patterns.

No longer `put box_own_prop γ P` in the invariant, it is persistent.

    The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.

Robbert Krebbers authored 8 years ago and Ralf Jung committed 8 years ago

We do this by introducing a type class UpClose with notation ↑.

The reason for this change is as follows: since `nclose : namespace
→ coPset` is declared as a coercion, the notation `nclose N ⊆ E` was
pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked
because type checking goes from left to right, and as such would look
for an instance `SubsetEq namespace`, which causes the right hand side
to be ill-typed.

Use COFEs only for the recursive domain equation solver

In particular, make sure we always try eassumption before reflexivity.

The old name didn't make much sense. Also now we can have
pure_False too.