Fix some longstanding renaming issues

This merge request attempts to fix some longstanding inconsistencies and stupidities in naming throughout the development. The reason that I created this merge request now, is that we are working on implementing !66 (merged) (generalized proof mode) and !71 (merged) (the plain modality), which both will result in even more modalities and subclasses of propositions of the logic.

Modalities and their corresponding type classes

The classes for properties of propositions and their corresponding modalities are used a lot. As such, they should have short and clear names. We now have have just classes/modalities for timeless and persistent properties, but we will have more when !66 (merged) and !71 (merged) are integrated. This MR makes two changes:

• The modalities are now the adverb of the type class, as proposed by @jung. This avoids a proliferation of names when more modalities/type classes are introduced.
• The suffixes P of the existing type classes TimelessP and PersistentP have been removed.

This gives rise to the following names for our type classes and modalities (including those in !66 (merged) and !71 (merged)):

Class	Property	Corresponding modality
Timeless P	▷ P ⊢ ◇ P	except_0, ◇ P := ▷ False ∨ P
Persistent P	P ⊢ □ P	persistently, □ P, defined in the model
Affine P	Q ⊢ emp	affinely, ■ P := emp ∧ P
Absorbing P	▲ P ⊢ P	absorbingly, ▲ P := True ∗ P
Plain P	P ⊢ ⋊ P	plainly, ⋊ P, defined in the model

Consistent capitalization

As proposed by @jung, we should consistently de-capitalize acronyms. We were already de-capitalizing some acronyms, like Ofe, at some places, but by far consistently. This MR fixes this situation, and now also de-capitalizes the following acronyms: Cmra, Ucmra, Sts and Dra. Hopefully I have fixed all acronyms and all uses thereof.

Properties of elements of algebraic structures

Since the names Persistent and Timeless are now used for persistent and timeless propositions, we have to do some renaming here:

Class	Property
Discrete x	∀ y, x ≡{0}≡ y → x ≡ y
Coreable x	pcore x ≡ Some x

Questions

• What symbols to use for the new modalities. I guess we can decide that in the other MRs.
• Should we rename except_0 into timelessly?
• There is still a proof mode tactic called iAlways. This one will also deal with the plain and affine modality, so the name should not become iPersistent or something like that. Do we have a better proposal for a name?