There are now two proof mode tactics for dealing with modalities:

- `iModIntro` : introduction of a modality
- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality

The behavior of these tactics can be controlled by instances of the `IntroModal`
and `ElimModal` type class. We have declared instances for later, except 0,
basic updates and fancy updates. The tactic `iMod` is flexible enough that it
can also eliminate an updates around a weakest pre, and so forth.

The corresponding introduction patterns of these tactics are `!>` and `>`.

These tactics replace the tactics `iUpdIntro`, `iUpd` and `iTimeless`.

Source of backwards incompatability: the introduction pattern `!>` is used for
introduction of arbitrary modalities. It used to introduce laters by stripping
of a later of each hypotheses.

And also rename the corresponding proof mode tactics.

docs: make the borders slightly larger

This makes it so that lines of text don't become so ridiculously long and are easier to read.

What do you think @robbertkrebbers @jjourdan ?

See merge request !17

docs: make the borders slightly larger, so that lines of text dont become so ridicolously long and are easier to read

Put the appendix under CC-BY 4.0

The title says this all. I hereby relicense my contributions to the appendix under the CC-BY 4.0 license.

For this to complete, I need similar statements from all other contributors: @robbertkrebbers @jjourdan @abizjak

See merge request !16