Big op lemmas `big_op{L,L2,M,M2,S}_intuitionistically_forall`

See merge request !560

Revert "Merge branch 'duplicable-type-class' into 'master'"

Closes #370

See merge request iris/iris!565

This reverts commit 71a1fbf0, reversing
changes made to ce12f3a6.

Mapsto notation changes: remove `l ↦ -`, and change `l ↦□ I` to `l ↦_I □`.

See merge request iris/iris!555

It is barely used and causes a lot of confusion when used like 'l ↦ - * P'

Add duplicable type class

See merge request iris/iris!481

Makefile: fix recursive invocation to use `$(MAKE)`

See merge request iris/iris!561

Calling `make` is known-bad in many cases, but never as much as here:

```
make[2]: Nothing to be done for `pre-all'.
touch theories/algebra/ofe.vo
touch theories/algebra/monoid.vo
touch theories/algebra/cmra.vo
[...]
touch theories/heap_lang/lib/array.vo
make[2]: Nothing to be done for `post-all'.
make[1]: *** wait: No child processes.  Stop.
gmake: *** [Makefile:3: all] Error 2
```

That is, `big_sepL2_intuitionistically_forall`, `big_sepL2_forall`, and
`big_sepM2_intuitionistically_forall`.

That is, `big_sepMS_intuitionistically_forall`, `big_sepMS_forall`,
`big_sepMS_impl`, and `big_sepMS_dup`.

Fix typos

See merge request iris/iris!559

Fix typos

See merge request iris/iris!557

Add library for monotonic nat ghost state

Closes #327

See merge request iris/iris!547

Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

Implemented as an algebra for rules about `auth max_natUR` and a
logic-level wrapper for the auth element (a nat) and fragment (a
persistent lower-bound).

Fixes #327.

Add swap lemmas for exist and forall

See merge request iris/iris!552