Front integration and various changes (#55)

* Integration mostly but roughly finished. Code compiles and is adapted to the change of variables representation in the kernel, except for two parts:
Unification is not fully working. It is used in many "tactics" deduction rules, expect some of those to not always work.
Fornt Macro: Compile-time string interpolation, with quote and so on. Probably easier to correct, but the syntax of that code is very difficult to understand. Dor now, this functionality is disabled (commented).

* simplifying, completting and consitentifying representations of schematic nodes in the Kernel. For now, Kernel compiles.

* More consistency and completeness changes. Code compile and tests outside the front do pass. Some tests related to unification and rules application in the front don't.

* Scaladoc up to date for the whole kernel.

* Removed the singleton set symbol from the definition of set theory. It should be an easily derived symbol. Added the missing subset axiom to set theory. Improved documentation for RunningTheory and Set Theory.

* Added a new deduction step: Rewrite True. it subsumes Hypothesis and is equivalent to rewriting a sequent that is OCBSL-true. Added top and bot constant predicate labels. Some more documentation.

* Rework of the user manual. Contains about everything Kernel-related. Does not contain documentation about the front, nor about the example development.

* Commented a test that can't pass until the unifier is repaired.

* remove leftover tentative code in Mapping.scala

* Make unification tests more readable:
* improve error messages when a test fails
* name emptyContext and emptyResult instead of using UnificationContext()
* split the expected unification result into a separate clause
  in the method to distinguish visually checkDoesNotUnify(a, b, partial)
  and checkUnifiesAs(a, b, expected)

* Split unification tests into multiple test cases

* @Ignore front's proof tests (instead of commenting out)

* Improve error messaging in front ProofTests

In particular, supply clues when assertions fail and split the tests into
test cases to clearly see which tests pass and which fail.

* Ignore unification tests until unification works with the new version of Lisa

* Run scalafix

* Further split unification tests: 1 test corresponds to 1 check

* Merge conflicts in the manual

* scalafix.

* scalafix 2.

* scalafix 3.

* trying to sastisfy the CI 5.

* Trying to satisfy the CI, 6.

* Trying to satisfy the CI, 7.

* Trying to satisfy the CI, 8.

* Front integration (#52)

* Large update to the user manual
* Merge development in Peano Arithmetic

* scalafix.

* Front integration (#53)

Reintroduce all of the front. 
Make the parser and printer working with the change on FOL..
Compatibility with the Peano Arithmetic development.
Update to the Manual.

Co-authored-by: Katja Goltsova <katja.goltsova@protonmail.com>