Lemmas stating that big ops are commuting with op/sep.

See merge request iris/iris!422

Document `%H` pattern.

Closes #305

See merge request iris/iris!423

Fix iIntros on forall

Closes #307

See merge request iris/iris!424

Fixes #307.

ASCII notation

Closes #270

See merge request iris/iris!396

- all ascii notation is marked "only parsing" so this PR shouldn't
  change anything for anyone using only unicode notation.
- the algorithm for creating an ascii notation is pretty simple.
  - \ast -> *
  - \triangleright -> |>
  - \vee -> \/
  - \wedge -> /\
  - \forall -> forall
  - \exists -> exists
  - \ast -> **

make names of more `f_op`/`f_core` rewrite lemmas more consistent

See merge request iris/iris!403

This closes issue #305.

Add support for pure names in intro patterns

Closes #88

See merge request iris/iris!400