diff --git a/src/docs/obsolete/ProB_Logic_Calculator_old.adoc b/src/docs/obsolete/ProB_Logic_Calculator_old.adoc
deleted file mode 100644
index bea5ff3fd954e3676238cfb5b0aff3feb0f0e231..0000000000000000000000000000000000000000
--- a/src/docs/obsolete/ProB_Logic_Calculator_old.adoc
+++ /dev/null
@@ -1,257 +0,0 @@
-
-[[prob-logic-calculator]]
-= ProB Logic Calculator
-
-WARNING: This section is relatively old and may contain errors.
-
-Below is a ProB-based http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html[logic
-calculator]. You can enter predicates and expressions in the upper
-window (<<summary-of-b-syntax,using B syntax>>), and then press the
-"Evaluate" button to ask ProB to evaluate the formula. Variables are
-assumed to be implicitly existentially quantified for the "Evaluate"
-button which tries to find solutions and universally quantified for the
-"Tautology Check" button which tries to find counter-examples. A
-series of examples for the "Evaluate" mode can be loaded from the
-examples menu. There is a <<small tutorial>> at the bottom
-of the page.
-
-http://wyvern.cs.uni-duesseldorf.de:8443/index.html[*Click here to get to the ProB Logic Calculator*]
-
-The calculator above has a time-out of 3 seconds, and `MAXINT` is set
-to 127 and `MININT` to -128. An alternative version of the calculator is
-available at the
-http://www.formalmind.com/en/blog/prob-logic-calculator[Formal Mind
-website]. You can also <<downloads,download ProB>> for execution on
-your computer, along with support for http://en.wikipedia.org/wiki/B[B],
-http://www.event-b.org/[Event-B],
-http://en.wikipedia.org/wiki/Communicating_sequential_processes[CSP-M],
-http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html[TLA+],
-and http://en.wikipedia.org/wiki/Z_notation[Z]. There are also 64-bit
-versions available for Linux and Mac (the above calculator only uses the
-32-bit version).
-
-[[short-syntax-guide-for-b-constructs]]
-== Short syntax guide for some of B's constructs:
-
-* comments `/* ... */`
-* conjunction `P & Q`, disjunction `P or Q`, implication `P \=> Q`,
-equivalence `P \<\=> Q`, negation `not(P)`, existential quantification
-`#x.(P)`, universal quantification `!x.(P\=>Q)`
-* equality `x=y`, disequality `x/=y`
-* boolean values `TRUE`, `FALSE`, converting predicate to value
-`bool(P)`; Warning: `TRUE` and `FALSE` are values and not predicates in
-B and cannot be combined using logical connectives.
-* strings "...", set of all strings `STRING`
-* arithmetic comparisons `x < y`, `x > y`, `x \<= y`, `x >= y`
-* membership `x:S`, not membership, `x/:S`, subset `S<:R`, strict subset
-`S <<: R`
-* arithmetic operators `x+y`, `x-y`, `x*y`, `x/y`, `x mod y`, `x**y` ,
-`succ(x)`, `pred(x)`
-* mathematical integers `INTEGER`, mathematical natural numbers
-`NATURAL`, implementable integers `INT`, implementable naturals `NAT`,
-maximum implementable integer `MAXINT`, minimum implementable integer
-`MININT`
-* empty set `{}`, set enumeration `{x,y,...}`, comprehension set defined
-by predicate `{x|P}`, lambda abstraction `%x.(P|E)`, interval `m..n`
-* set union `S \/ T`, set intersection `S /\ T`, set difference `S - T`,
-power set `POW(S)`, Cartesian product `S*T`, cardinality of set
-`card(S)`
-* set of relations between two sets `S \<\-> T`, set of partial functions
-`S +\-> T`, set of total functions `S -\-> T`
-* relational image `r[S]`, relational composition `(r1 ; r2)`,
-transitive closure `closure1(r)`, identity relation over a set `id(S)`,
-domain of a relation `dom(r)`, its range `ran(r)`, its inverse `r~`,
-relational overriding `r1 <+ r2`
-* empty sequence `[]`, explicit sequence `[x,y,...]`, concatenation
-`s1^s2`, first element `first(s)`, tail `tail(s)`, prepend an element
-`E\->s`, size of a sequence `size(s)`
-* sets of sequences over a set `seq(S)`, set of injective sequences
-`iseq(S)`, set of permutations `perm(S)`
-
-More details can be found on our <<summary-of-b-syntax,page on the B syntax>>.
-
-NOTE: Statements (aka substitutions) and B machine construction
-elements cannot be used above; you must enter either a predicate or an
-expression.
-
-The term logic calculator we use is taken from
-http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html[Leslie
-Lamport]. An early implementation of a logic calculator is the
-http://en.wikipedia.org/wiki/William_Stanley_Jevons#Logic[Logic Piano].
-
-We are grateful for feedback about our logic calculator (send an email
-to https://www.cs.hhu.de/lehrstuehle-und-arbeitsgruppen/softwaretechnik-und-programmiersprachen/unser-team.html[Michael Leuschel]). In
-future we plan to provide additional features:
-
-* getting an unsat core for unsatisfiable formulas
-* better feedback for syntax and type errors
-* graphical visualization of formulas and models
-* support for alternative input syntax, such as
-http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html[TLA+]
-or http://en.wikipedia.org/wiki/Z_notation[Z]
-* ability to change the parameters, e.g., use the
-https://www3.hhu.de/stups/downloads/pdf/PlaggeLeuschel_Kodkod2012.pdf[ProB-Kodkod
-backend] instead of the default constraint-logic programming kernel.
-
-[[small-tutorial]]
-== Small Tutorial
-
-Here is a small tutorial to get you started. B distinguishes
-expressions, which have a value, and predicates which can be either true
-or false. First, let us type an expression:
-
-....
-1+1
-....
-
-The calculator returns the value `2`. A more complicated expression is:
-
-....
-{1,2,3} \/ {1+2+3}
-....
-
-which has the value `{1,2,3,6}`. Now, let us type a simple predicate:
-
-....
-1>2
-....
-
-The calculator tells us that this predicate is false. We can combine
-predicates using the logical connectives. For example, the following
-predicate is true:
-
-....
-1>2 or 2>1
-....
-
-We can also use existential quantification to produce a predicate:
-
-....
-#(x).(x+10=30)
-....
-
-which is true and ProB will give you a solution `x=20`. In the
-calculator, any variable that is not explicitly introduced is considered
-existentially quantified. Thus, you get the same effect by simply
-typing:
-
-....
-x+10=30
-....
-
-If you want to get all solutions for the equation x+10=30, you can make
-use of a set comprehension:
-
-....
-{x|x+10=30}
-....
-
-Here the calculator will compute the value of the expression to be
-`{20}`, i.e., we know that 20 is the only solution for `x`. Note that
-the B language has Boolean values `TRUE` and `FALSE`, but these are not
-considered predicates in B. Thus if we type:
-
-....
-TRUE
-....
-
-this is considered an expression and not a predicate. This also means
-that `TRUE or FALSE` is not considered a legal predicate in pure B.
-However, the logic calculator accepts this and as such you can type:
-
-....
-TRUE or FALSE
-....
-
-which is determined to be true. In pure B, you would have to write
-something like:
-
-....
-1=1 or 1=2
-....
-
-Finally, in pure B, variables can only range over values in B, not over
-predicates. Thus `P or Q` is not allowed in pure B, but our logic
-calculator does accept it. As such you can type
-
-....
-P or Q
-....
-
-which is equivalent to typing
-
-....
-P=TRUE or Q=TRUE
-....
-
-If you want to find all models of the formula, you can use a set
-comprehension:
-
-....
-{P,Q | P or Q}
-....
-
-Also, if you want to check whether your formula is a tautology you can
-press the "Tautology Check" button. In this case (for `P or Q`) a
-counter example is produced by the tool. More generally, you can check
-proof rules using the "Tautology Check" button. E.g., our tool will
-confirm that the following is a tautology:
-
-....
-(A => B) & not(B) => not(A)
-....
-
-Note, however, that our tool is not a prover in general: you can use it
-to find solutions and counter-examples, but in general it cannot be used
-to prove formulas using variables with infinite type. In those cases,
-you may see enumeration warnings in the output, which means that ProB
-was only able to check a finite number of values from an infinite set.
-This could mean that the result displayed is not correct (even though in
-general solutions and counter-examples tend to be correct; in future we
-will refine ProB's output to also indicate when the
-solution/counter-example is still guaranteed to be correct)!
-
-[[executing-the-calculator-locally]]
-== Executing the Calculator locally
-
-You can evaluate formulas on your machine in the same way as the
-calculator above, by <<downloads,downloading ProB>> (ideally a nightly
-build) and then executing one of the following commands:
-
-....
-./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_file MYFILE
-....
-
-The above command requires you to put the formula into a file `MYFILE`.
-The command below allows you to put the formula directly into the
-command:
-
-....
-./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval "MYFORMULA"
-....
-
-If you want to perform the tautology check you have to do the following:
-
-....
-./probcli -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128 -p TIME_OUT 500 -eval_rule_file MYFILE
-....
-
-You can of course adapt the preferences (TIME_OUT, MININT, MAXINT, ...)
-according to your needs; the
-<<using-the-command-line-version-of-prob,user manual>> provides more
-details.
-
-....
-rlwrap ./probcli -repl -p BOOL_AS_PREDICATE TRUE -p CLPFD TRUE -p MAXINT 127 -p MININT -128
-....
-
-Probably, you may want to generate full-fledged B machines as input to
-`probcli`. This allows you to introduce enumerated and deferred sets;
-compared to using sets of strings, this has benefits in terms of more
-stringent typechecking and more efficient constraint solving.
-
-An alternate web interface is currently being developed
-http://cobra.cs.uni-duesseldorf.de/evalB/[here]. Its code is available
-at
-https://github.com/bendisposto/evalB[`https://github.com/bendisposto/evalB`]
-and it can easily be run locally using `gradle jWR`.
diff --git a/src/docs/obsolete/Tutorial_Unit_Plugin.adoc b/src/docs/obsolete/Tutorial_Unit_Plugin.adoc
deleted file mode 100644
index ff2ac0be189e0988740eb07491aee99d279fe852..0000000000000000000000000000000000000000
--- a/src/docs/obsolete/Tutorial_Unit_Plugin.adoc
+++ /dev/null
@@ -1,114 +0,0 @@
-
-[[tutorial-unit-plugin]]
-= Tutorial Unit Plugin
-
-Note: This feature is no longer available in ProB 1.9.0.
-
-This tutorial describes, how ProB's integrated plugin for unit analysis
-can be used to verify the usage of physical units throughout a B
-machine. This includes
-
-1.  Annotating variables with their physical unit,
-2.  Infer the unit of variables without an annotation,
-3.  Detect incorrect usage of units, like addition of differently
-annotated variables.
-
-The plugin is currently a work in progress. Rough edges are to be
-expected.
-
-We assume that you have a general understanding of B and the usage of
-ProB.
-
-[[activating-the-plugin-and-setting-preferences]]
-== Activating the Plugin and setting preferences
-
-Currently, the plugin can only be used with classical B machines.
-Therefore, a B machine needs to be loaded before the plugin can be
-activated.
-
-Once a machine is loaded, the plugin can be activated through ProB's
-plugin menu. Choose "Interpreting units stored in pragmas" inside of
-the activate plugin submenu. Furthermore, the preferences can be
-accessed through the menu.
-
-At this stage, two preferences can be set:
-
-1.  Activation or deactivation of a static pre-check, that is run once a
-machine is loaded and performs a fix point analysis of the formerly
-mentioned usages.
-2.  The maximal number of iterations that are performed, before the fix
-point algorithm stops.
-
-If the static pre-check is activated, the plugin moves the animator into
-a fix point state, in which possible unit errors are presented to the
-user through ProB's error reporting facilities.
-
-[[annotating-variables-and-animating-a-machine]]
-== Annotating variables and animating a machine
-
-To connect a variable with an expected physical unit, a special comment
-is placed before the variable.
-
-....
-VARIABLES
-  /*@ unit "10**1 * m**1" */ x
-  /*@ unit "m**2"*/ y
-....
-
-Following the "unit" keyword is a specification of the unit in form of
-a B expression. Allowed constructs are multiplication and division as
-well as exponentiation.
-
-For several often used units like cm, dm, km, etc. an alias can be used.
-
-....
-VARIABLES
-  /*@ unit "mm" * / x,
-  /*@ unit "dm" * / y
-....
-
-Once at least one variable is annotated, further units can be inferred.
-
-The unit plugin integrates with ProB's animation facilities. Both
-results and parameters of operations are displayed with their unit. For
-variables, the unit is stored inside the machines state space. This
-enables the plugin to be used in conjunction with the evaluation view,
-the dot output and most other ProB features.
-
-[[converting-between-units]]
-== Converting between units
-
-To distinct between a numerical multiplication, that changes the values
-without changing the unit and a multiplication meant to convert between
-units, a second pragma is added. To convert between units, add the
-respective conversion factor and mark the multiplication as a unit
-conversion.
-
-See the following B machine for an example operation:
-
-....
-MACHINE SimpleConversion
-VARIABLES
-  /*@ unit "10** -2 *m"*/ xx,
-  /*@ unit "10** -3 *m"*/ yy,
-converted
-INVARIANT
-  xx:NAT &
-  yy:NAT &
-  converted:NAT
-INITIALISATION xx,yy,converted:=0,0,0
-OPERATIONS
-  n <-- addToXX = n:=xx+1;
-  mmToCm  = converted:=/*@ conversion */(10*yy)
-END
-....
-
-[[static-analysis]]
-== Static analysis
-
-If activated, the results of the static analysis can be accessed from
-the plugin menu. Currently, the results include the inferred unit of
-every variable inside the active B machine. Furthermore, a warning is
-displayed, if multiple units were inferred for a single variable (which
-usually is caused by wrong usage of the variable). Another warning
-message is shown for variables, for which no unit could be inferred.