was not a valid expression, meaning that
once a :let was defined in Event-B mode
every command expecting an expression
failed with an error

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

\newcommand doesn't allow overwriting an existing definition. It worked
fine in Jupyter Notebook, which uses MathJax, which apparently doesn't
actually check this. However, it causes errors in VS Code, which uses
KaTeX. It probably also caused errors when converting a notebook to
LaTeX and typesetting it with a proper LaTeX implementation.

\def overwrites any existing definition and so should work in all cases.

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

The already released version 1.3.0 still needs to be installed this way.

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

Previously the entire remaining line was considered an error, which is
unnecessary most of the time when there's only one incorrect character
that can be easily skipped.

This allows using Jupyter's Python API to install the kernel. It returns
the location of the newly installed kernelspec, which allows copying the
kernel jar file into the kernelspec directory instead of the ProB home
directory. This is cleaner and allows fully uninstalling the kernel
using a single command.

Additionally, we no longer depend on Guice to generate the kernel.json
(we use Python's json module instead) and no longer use the deprecated
Main.getProBDirectory method from ProB 2.

The Python script for installing the kernel is bundled into the kernel
jar as __main__.py, which allows running the jar file using Python. The
installation can still be started using Java, in which case the jar
re-executes itself using Python. Yes, this is a little bit cursed, but
it works.

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

If there is no detailed error information, it now always returns an
empty list and never null.

Now that ProB supports reals, an expression like x>y is no longer
sufficient to infer that x and y are integers.

LaTeX formulas inside tables cause various layout issues in Jupyter
Notebook, such as long sets being wrapped even when they would fit on a
single line, table columns being wider than necessary, and LaTeX
formulas being left-aligned instead of right-aligned like normal text.

In some cases, ProB apparently "unwraps" LET predicates as well,
not just existential quantifications.