diff --git a/src/docs/chapter/user/40_AdvancedFeatures/00_section_header.adoc b/src/docs/chapter/user/40_AdvancedFeatures/00_section_header.adoc
deleted file mode 100644
index 682deae961ed15b77b83662d4e29baefe69028a7..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/00_section_header.adoc
+++ /dev/null
@@ -1,7 +0,0 @@
-
-[[advanced-features]]
-= Advanced Features
-:leveloffset: +1
-
-Over the years, the ProB Team developed a few features for advanced users.
-You can find further descriptions and tutorials on how to use them in the following sections.
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/00_section_header.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/00_section_header.adoc
deleted file mode 100644
index df0714c37873281719bd0270263262c48136ba5f..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/00_section_header.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-
-[[feature-description]]
-= Feature Description
-:leveloffset: +1
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/01_Bash_Completion.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/01_Bash_Completion.adoc
deleted file mode 100644
index 94353ac658bcaca277709b83e62a6c5efc2749d7..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/01_Bash_Completion.adoc
+++ /dev/null
@@ -1,35 +0,0 @@
-
-[[bash-completion]]
-= Bash Completion
-
-For the http://en.wikipedia.org/wiki/Bash_(Unix_shell)[Bash] Unix Shell
-we provide command completion support.
-
-Example
-
-....
-$ probcli -re
--refchk  -repl
-....
-
-[[installation-bash-completion]]
-== Installation
-
-A generated version of the command completion for Bash is available
-http://nightly.cobra.cs.uni-duesseldorf.de/bash/prob_completion.sh[here].
-To install download the linked file and store it locally on your
-machine. To enable the completion you need to *source* the file.
-
-....
-$ source
-....
-
-To enable the completion automatically add the line above to your Bash
-settings, e.g. in the *.bashrc* or *.profile* files in your home
-directory.
-
-[[contributing]]
-== Contributing
-
-Bugs and improvements can be submitted on the project's
-https://github.com/bivab/prob_bash_completion[GitHub Page]
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/02_Common_Subexpression_Elimination.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/02_Common_Subexpression_Elimination.adoc
deleted file mode 100644
index 269c27234ab8486b111bdb4046e8d169018d4e13..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/02_Common_Subexpression_Elimination.adoc
+++ /dev/null
@@ -1,112 +0,0 @@
-
-[[common-subexpression-elimination]]
-= Common Subexpression Elimination
-
-As of version 1.5.1 ProB supports
-https://en.wikipedia.org/wiki/Common_subexpression_elimination[common
-subexpression elimination (CSE)].
-
-[[basics-of-cse]]
-== Basics of CSE
-
-To enable CSE you need to set the advanced preference `CSE` to true
-(this can be done using the switch `-p CSE TRUE` when using the
-<<using-the-command-line-version-of-prob,command-line version
-probcli>> or using the Advanced Preferences command in ProB Tcl/Tk). With
-CSE enabled, ProB will translate the predicate
-
-`x:dom(f(a)) & r=f(a)(x)`
-
-into
-
-`(LET @0==(f(a)) IN x ∈ dom(@0) ∧ r = @0(x))`
-
-before evaluating it. As you can see, the common sub-expression `f(a)`
-has been lifted into a LET statement. This has the advantage that the
-expression `f(a)` will only get evaluated once (rather than twice, in
-case `x:dom(f(a))`). Identifiers introduced by the CSE always start with
-the @-sign. As another example, the predicate
-
-`x*x+2*x > y*y*y & y*y*y > x*x+2*x`
-
-gets translated into
-
-`LET @2==(x*x+2*x) IN (LET @4==((y*y)*y) IN @2 > @4 & @4 > @2))`
-
-You may observe that the B-language does not have a let-construct for
-expression nor predicates (only for substitutions). There are various
-ways one can overcome this (e.g., using an existential quantifier for a
-predicate), but ProB adds its own LET-construct to the language in the
-interpreter. Moreover, to avoid issues with well-definedness and
-ensuring that ProB only evaluates the LET expressions when really
-needed, this LET has a different behaviour than the "standard"
-constructs. Indeed, ProB's LET is lazy, i.e., it will only evaluate the
-expression when required by the computation of the body of the LET. For
-example, in
-
-`LET @1==f(a) IN 2>3 & @1+@1>10`
-
-the expression `f(a)` will never be evaluated. This is important for
-well-definedness (e.g., suppose a is not in the domain of f) and for
-performance.
-
-[[substitutions]]
-== Substitutions
-
-To enable CSE also inside substitutions (aka B statements) you need to
-set the preference `CSE_SUBST` to true. By default, the CSE will only be
-applied to top-level predicates, such as the invariant, the assertions,
-the properties or individual predicates inside operations (but not the
-operation as a whole).
-
-[[sharing-predicates]]
-== Sharing Predicates
-
-By default ProB's CSE will also share predicates. You can turn off CSE
-for predicates, i.e., only expressions get shared, by setting the
-preference `CSE_PRED` to `FALSE`. For example, by default ProB's CSE
-will translate
-
-`x+1 > 10 & (x+1 > 10 => y=22)`
-
-into
-
-`LET @1==(x + 1 > 10) IN @1 & (@1 => y = 22)`
-
-After setting `CSE_PRED` to `FALSE`, this will be translated into:
-
-`LET @0==(x + 1) IN @0 > 10 & (@0 > 10 => y = 22)`
-
-[[other-preferences]]
-== Other Preferences
-
-ProB will also share expressions which are potentially not well-defined,
-and takes extra care with those expressions (in particular in the
-context of set comprehensions and quantifications). However, you can
-completely turn off sharing of potentially not-well defined expressions
-by setting the preference `CSE_WD_ONLY` to `TRUE`. For example, by
-default the following predicate
-
-`x>1 & 100/x > 20 & 100/x <26`
-
-will get translate into
-
-`LET @0==(100 / x) IN (x > 1 & @0 > 20) & @0 < 26)`
-
-and ProB will find the solution `x=4`. With `CSE_WD_ONLY` to `TRUE`, the
-predicate will be left unchanged (and ProB will find the same solution).
-
-[[tips]]
-== Tips
-
-To inspect the effect of CSE, you do one of the following:
-
-* In ProB Tcl/Tk you can use the command "Show Internal
-Representation" in the Debug menu to inspect the effect of CSE on your
-machine
-* For probcli, you can use the command `-pp FILE` to write the
-pretty-printed internal representation of your machine after CSE to a
-file
-* For the REPL of probcli (command -repl), you can use the option
-`-p REPL_UNICODE TRUE` to force ProB to print your
-expressions/predicates after CSE processing (using Unicode characters)
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/03_PROBPATH.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/03_PROBPATH.adoc
deleted file mode 100644
index 8a4bbc75f9fd736b4339884179169951b1f86923..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/03_PROBPATH.adoc
+++ /dev/null
@@ -1,32 +0,0 @@
-
-[[probpath]]
-= PROBPATH
-
-Starting with version 1.5 of ProB, it is possible to customize where the
-parser will ProB will search for referenced files.
-
-By default ProB will try to find files referenced from a machine (using
-SEES, INCLUDES, DEFINITON-files, etc) resolving paths as relative to the
-current machine or within the ProB standard library.
-
-Commonly used files can be placed in a shared location, e.g. in the
-standard library (the stdlib directory in the ProB distribution) or any
-custom location.
-
-The search path can be customized by defining a PROBPATH environment
-variable that contains a list of directories to be searched. On windows
-the directors are separated by a ";" and on unix systems by a ":"
-character, e.g.:
-
-On unix:
-
-`PROBPATH=\~/myproject/common:~/myotherproject/common probcli model.mch`
-
-And on windows:
-
-`PROBPATH=\~/myproject/common;~/myotherproject/common probcli model.mch`
-
-will resolved referenced files relative to model.mch, then in
-*~/myproject/common* then in *~/myotherproject/common* and finally in
-the standard library of ProB, stopping as soon as a file with the name
-being looked up is found.
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/04_TLC.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/04_TLC.adoc
deleted file mode 100644
index d5214c46c89662dd1b44fd4c0784baf434ddff52..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/04_TLC.adoc
+++ /dev/null
@@ -1,144 +0,0 @@
-
-[[tlc]]
-= TLC
-
-As of version 1.4.0, ProB can make use of
-http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html[TLC]
-as an alternative model checker to validate B specifications. TLC is an
-efficient model checker for TLA+ specifications, which can check LTL
-properties with fairness. It is particularly good for lower level
-specifications, where it can be substantially faster than ProB's own
-model checker. TLC has been released as an open source project, under
-the
-http://research.microsoft.com/en-us/um/people/lamport/tla/license.html[MIT
-License].
-
-[[how-to-use-tlc]]
-== How to use TLC
-
-[[using-tlc-in-prob-tcltk]]
-=== Using TLC in ProB Tcl/Tk
-
-First you have to open a B specification in the ProB GUI. Then you can
-select the menu command "Model Check with TLC" in the
-"Verify->External Tools" menu.
-
-image::Model_Checking_With_TLC.png[]
-
-You can use TLC to find the following kinds of errors in the B
-specification:
-
-* Deadlocks
-* Invariant violations
-* Assertion errors
-* Goal found (a desired state is reached)
-* Properties violations (i.e, axioms over the B constants are false)
-* Well-definedness violations
-* Temporal formulas violations
-
-In some cases, TLC reports a trace leading to the state where the error
-(e.g. deadlock or invariant violation) occur. Such traces are
-automatically replayed in the ProB animator (displayed in the history
-pane) to give an optimal feedback.
-
-image::Model_Checking_With_TLC_Trace.png[]
-
-[[requirements]]
-==== Requirements
-
-On Linux the tlc-thread package is required to run TLC from the tcl/tk
-ui:
-
-`sudo apt-get install tcl-thread`
-
-[[using-tlc-in-probcli]]
-=== Using TLC in probcli
-
-You can use the following switch to use TLC rather than ProB's model
-checker:
-
-`-mc_with_tlc`
-
-Some of the standard probcli options also work for TLC:
-
-* -noinv (no invariant checking)
-* -nodead (no deadlock checking)
-* -noass (no assertion checking)
-* -nogoal (no checking for the optional goal predicate)
-
-In addition you can provide
-
-* -noltl (no checking of LTL assertions)
-
-The preference `TLC_WORKERS` influences the number of workers that will
-be used by TLC. So, a call might look like this:
-
-`probcli FILE.mch -mc_with_tlc -p TLC_WORKERS 2 -noltl`
-
-[[when-to-use-tlc]]
-== When to use TLC
-
-TLC is extremely valuable when it comes to explicit state model checking
-for large state spaces. Otherwise, TLC has no constraint solving
-abilities.
-
-[[translation-from-b-to-tla]]
-Translation from B to TLA+
---------------------------
-
-TLC is a very efficient model checker for specifications written in
-http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html[TLA+].
-To validate B specification with TLC we developed the translator TLC4B
-which automatically translates a B specification to TLA+, invokes the
-model checker TLC, and translates the results back to B. Counter
-examples produced by TLC are double checked by ProB and replayed in the
-ProB animator. The translation to TLA+ and back to B is completely
-hidden to the user. Hence, the user needs no knowledge of TLA+ to use
-TLC.
-
-There is a
-http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport[technical
-report] that describes our translation from B to TLA+.
-
-[[limitations-tlc]]
-== Limitations
-
-The following constructs are currently not supported by the TLC4B
-translator:
-
-* Refinement specifications
-* Machine inclusion (SEES, INCLUDES, ..)
-* Sequential composition statement (G;H)
-
-[[visited-states]]
-== Visited States
-
-Sometimes TLC will show a different number of visited states compared to
-the ProB model checker. The following example should illustrate this
-issue:
-
-....
-MACHINE NumberOfStates
-CONSTANTS k
-PROPERTIES
-k : 1..10
-VARIABLES x
-INVARIANT
-x : NATURAL
-INITIALISATION x := k
-END
-....
-
-ProB will report 21 distinct states (1 root state, 10 constant setup
-states, 10 initialization states):
-
-image::NumberOfStates.jpeg[]
-
-TLC will only report 10 distinct states (10 initialization states).
-
-[[more-information]]
-== More Information
-
-More information can be found in our
-https://www3.hhu.de/stups/downloads/pdf/HansenLeuschel_ABZ14.pdf[ABZ'14
-article].
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/ZZ_section_footer.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/ZZ_section_footer.adoc
deleted file mode 100644
index 909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/ZZ_section_footer.adoc
+++ /dev/null
@@ -1,2 +0,0 @@
-
-:leveloffset: -1
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/00_section_header.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/00_section_header.adoc
deleted file mode 100644
index de7acf42b5f29a88672d0706ad4cc811df14bba7..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/00_section_header.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-
-[[using-prob]]
-= Using ProB
-:leveloffset: +1
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Generating_Documents_with_ProB_and_Latex.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Generating_Documents_with_ProB_and_Latex.adoc
deleted file mode 100644
index 5e70f08f5df899433fb12ea064d6e4a68f24cf64..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Generating_Documents_with_ProB_and_Latex.adoc
+++ /dev/null
@@ -1,107 +0,0 @@
-
-[[generating-documents-with-prob-and-latex]]
-= Generating Documents with ProB and Latex
-
-ProB can (as of version 1.6.1) be used to process Latex files, i.e., the
-command-line tool probcli scans a given Latex file and replaces certain
-commands by processed results.
-
-[[usage-generating-documents]]
-== Usage
-
-A typical usage would be as follows:
-
-....
-   probcli FILE -init -latex Raw.tex Final.tex
-....
-
-Note: the FILE and -init commands are optional; they are required in
-case you want to process the commands in the context of a certain model.
-Currently the probcli Latex commands mainly support B and Event-B
-models, TLA+ and Z models can also be processed but all commands below
-expect B syntax. You can add more commands if you wish, e.g., set
-preferences using `-p PREF VAL` or run model checking `--model-check`.
-The Latex processing will take place after most other commands, such as
-model checking.
-
-You will probably want to put the probcli call into a Makefile, in
-particular when you want to generate dot graphics using ProB.
-
-The distribution folder of ProB contains an example with a Makefile,
-producing the following file, which at the same time documents the core
-features:
-
-https://www3.hhu.de/stups/prob/images/7/7f/Prob_latex_doc.pdf[ProB Latex Documentation]
-
-[[commands]]
-== Commands
-
-The commands are described in the PDF document above. Here is a short
-summary of some of the commands:
-
-* `\probexpr{EXRP}` command takes a B expression `EXPR`as argument and
-evaluates it. By default it shows the B expression and the value of the
-expression. Example: `\probexpr` will be replaced by `{1,1024}`
-** `ascii` to print the result as ASCII rather than using Latex math
-symbols
-** `time` to display the time taken for the command
-** `string` the result value is a string, and do not print the quotes
-around the string
-** `value` to just print the value, not the expression
-
-* `\probrepl{CMD}` command takes a probcli REPL command `CMD` as
-argument and executes it. By default it shows only the output of the
-execution, e.g., in case it is a predicate TRUE or FALSE. Example:
-`\probrepl{let DOM = 1..3}`. A variation of the latter is the new
-command `\problet{DOM}{1..3}` which shows the let construct itself
-within the generated Latex. Optional arguments for `\probrepl` are :
-** `solution` to display the solution bindings (for existential
-variables) found by ProB
-** `store` to store the solution bindings as local variables (similar to
-let)
-** `ascii` to print the result as ASCII rather than using Latex math
-symbols
-** `time` to display the time taken for the command
-** `print` to print the expression/predicate being evaluated
-(automatically set by `\problet`
-** `silent` to not print the result of the evaluation
-
-* `\probtable{EXRP}` command takes a B expression `EXPR`as argument,
-evaluates it and shows it as a Latex table. Optional arguments are
-`no-tabular`, `no-hline`, `no-headings`, `no-row-numbers`,
-`max-table-size=NR`.
-
-* `\probdot{DOT}{File1}` command takes a B expression `EXPR`as argument,
-evaluates it as a graph and writes a dot file `File1`. You can provide a
-second File as argument, in which case `dot` is called to generate a PDF
-document. You can also set `sfdp` as third argument, in which case the
-`sfdp` tool will be used instead of `dot`.
-
-* `\probprint{EXRP}` command takes a B expression or predicate `EXPR`as
-argument and pretty prints it. Optional arguments are:
-** `pred` only try to parse first argument as predicate
-** `expr` only try to parse first argument as expression
-** `ascii` to print the result as ASCII rather than using Latex math
-symbols
-
-* `\probif{EXPR}{Then}{Else}` command takes an expression or predicate
-`EXPR` and two Latex texts. If the expression evaluates to TRUE the
-first branch `Then` is processed, otherwise the other one `Else` is
-processed.
-
-* `\probfor{ID}{Set}{Body}` command takes an identifier `ID`, a set
-expression `Set` and a Latex text `Body`, and processes the Latex text
-for every element of the set expression, setting the identifier to a
-value of the set.
-
-[[some-examples]]
-== Some Examples
-
-* Presentation held in Grenoble in September 2016 about "Constraint
-Programming Puzzles in B"
-
-https://www3.hhu.de/stups/prob/images/2/2d/Puzzle_latex_presentation.pdf[Puzzle Latex Presentation]
-
-* SBMF'2016 keynote article:
-
-https://www3.hhu.de/stups/prob/images/1/17/Sbmf_2016_latex.pdf[Formal Model-Based Constraint Solving and Document Generation]
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Atelier_B.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Atelier_B.adoc
deleted file mode 100644
index 0fdd9576f1270dfd54be6aaaccc98da4fabfb72f..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Atelier_B.adoc
+++ /dev/null
@@ -1,95 +0,0 @@
-
-[[using-prob-with-atelier-b]]
-= Using ProB with Atelier B
-
-As of version 1.3,
-ProB contains a much improved parser which tries be compliant with
-Atelier B as much as possible.
-
-[[atelier-b-plugin]]
-== Atelier B Plugin
-
-There is also a
-http://tools.clearsy.com/tools/atelier-b-4-0-gui/external-tools-integration/prob-etool-generation/[plugin
-for Atelier B] for use withthe standalone Tcl/Tk Version on
-http://www.atelierb.eu/[Atelier B] projects.
-
-[[differences-with-atelier-b]]
-== Differences with Atelier B
-
-[[extra-features-of-prob]]
-=== Extra Features of ProB
-
-* Identifiers: ProB also allows identifiers consisting of a single
-letter. ProB also accepts enumerated set elements to be used as
-identifiers.
-
-* Lexing: The Atelier-B parser (`bcomp`) reports a lexical error
-(`illegal token |-`) if the vertical bar (|) of a lambda abstraction is
-followed directly by the minus sign.
-
-* Typing:
-** ProB makes use of a unification-based type inference algorithm. As
-such, typing information can not only flow from left-to-right inside a
-formula, but also from right-to-left. For example, it is sufficient to
-type `xx<:yy & yy<:NAT` instead of typing both `xx` and `yy` in ProB.
-** Similar to Rodin, ProB extracts typing information from all
-predicates. As such, it is sufficient to write `xx/:{1,2}` to assign a
-type to `xx`.
-** the fields of records are normalized (sorted); hence the predicate
-`rec(a:0,b:1) = rec(b:y,a:x)` is correctly typed for ProB.
-
-* DEFINITIONS: the definitions and its arguments are checked by ProB. We
-believe this to be an important feature for a formal method language.
-However, as such, every DEFINITION must be either a predicate, an
-expression or a substitution. You *cannot* use, for example, lists of
-identifiers as a definition. Also, for the moment, the arguments to
-DEFINITIONS have to be expressions. Finally, when replacing DEFINITIONS
-the associativity is not changed. E.g., with `PLUS(x,y) == x+y`, the
-expression `PLUS(2,3)*10` will evaluate to 50 (and not to 32 as with
-Atelier-B).
-
-* for a LET substitution, Atelier-B does not allow introduced
-identifiers to be used in the right-hand side of equations; ProB allows
-`LET x,y BE x=2 & y=x*x IN ... END`
-
-* ProB allows WHILE loops and sequential composition in abstract
-machines
-
-* ProB now allows the IF-THEN-ELSE for expressions with parentheses
-around it: `(IF x<0 THEN -x ELSE x END)`
-
-[[limitations-with-atelierb]]
-=== Limitations
-
-* Parsing: ProB will require parentheses around the comma, the
-relational composition, and parallel product operators. For example, you
-cannot write `r2=rel;rel`. You need to write `r2=(rel;rel)`. This allows
-ProB to distinguish the relational composition from the sequential
-composition (or other uses of the semicolon).
-
-* <<well-definedness-checking,Well-definedness>>: ProB will try to
-check if your predicates are well-defined during animation or model
-checking. For this ProB assumes (similar to Rodin) a stricter
-left-to-right definition of well-definedness than Atelier B.
-
-* Closure: The transitive and reflexive closure operator of classical B
-is not supported as defined in the B-Book by Abrial. AtelierB also does
-not support the operator as defined in the B-Book (as this version
-cannot be applied in practice). For the reflexive component of closure,
-ProB will compute the elements in the domain and range of the relation.
-
-Note however, that the transitive closure operator `closure1` is fully
-supported, and hence one can translate an expression `closure(e)`, where
-e is a binary relation over some domain d, into the expression
-`closure1(e) \/ id(d`).
-
-* Unsupported Operators:
-** Trees and binary trees: most but not all tree operators (mirror,
-infix) are supported yet (the `STRING` type is now supported);
-** `VALUES`: This clause of the `IMPLEMENTATION` machines is not yet
-supported;
-
-* There are also some general limitations wrt refinements. See
-<<current-limitations,Current
-Limitations section>> for more details.
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_KODKOD.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_KODKOD.adoc
deleted file mode 100644
index bfea468d07c43ef17258cf6df2fdf396f3c32676..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_KODKOD.adoc
+++ /dev/null
@@ -1,121 +0,0 @@
-
-[[using-prob-with-kodkod]]
-= Using ProB with KODKOD
-
-As of version 1.3.5 ProB can make use of
-http://alloy.mit.edu/kodkod/[Kodkod] as an alternate way of solving
-constraints. Kodkod provides a relational interface to SAT solvers and
-is the heart of the http://alloy.mit.edu/alloy/[Alloy] tool.
-
-[[how-to-enable-kodkod]]
-== How to enable Kodkod
-
-For the command-line version you need to call prob as follows:
-
-`probcli -p KODKOD TRUE`
-
-Note: to experiment with Kodkod you may want to try out the command:
-
-`probcli -p KODKOD TRUE -repl`
-
-If in addition you want see a graphical representation of the solutions
-found you can use the following command and open the `out.dot` file
-using dotty or GraphViz:
-
-`probcli -p KODKOD TRUE -repl -evaldot ~/out.dot`
-
-For the ProB Tcl/Tk Version you should select the menu command "Enable
-Kodkod for Properties" in the _Preferences_ menu.
-
-[[what-can-be-translated-kodkod]]
-== What can be translated
-
-* Types:
-** Basic Types: Deferred Sets, enumerated sets, integers, booleans
-** Sets of basic types
-** Relations between basic types
-** Higher-order types (sets of sets) are not supported
-
-* Operators:
-** Predicates: &, or, \=>, \<\=>, not, !, #, =, /=
-** Booleans: TRUE, FALSE, BOOL, bool(...)
-** Sets: \{..,...} \{x|P}, POW, card, Cartesian product, \/, /\, -, :,
-/:, /<:, <<: /<<:
-** Numbers: n..m, >, <, >=, <=, +, -, *, SIGMA(x).(P|x)
-** Relations: \<\->, |\->, dom, ran, id, <|, <<|, |>, |>>, ~, [...], <+,
-prj1, prj2, closure1
-** x : S+\->T, x:S-\->T, ..., lambda
-** currently no operations on sequences are supported
-
-* Some limitations:
-** If integers are used, a predicate can only be translated if a static
-analysis can estimate the interval of its possible values.
-** Generally only complete predicates are translated or nothing at all,
-unless you set the `KODKOD_ONLY_FULL` preference to FALSE.
-
-[[when-is-the-kokod-translation-used]]
-== When is the Kokod translation used
-
-Once enabled, the Kodkod translation will be used in the following
-circumstances:
-
-* for solving PROPERTIES
-* constraint-based assertion checking (`-cbc_assertions` command for
-`probcli` or the "Check Assertions on Constants" command in the menu
-_Verify_ -> Constraint-Based Checking)
-* constraint-based deadlock checking
-* in the <<eval-console,Eval Console>> in the ProB Tcl/Tk version
-* for the REPL in probcli (`probcli -p KODKOD TRUE -repl`)
-
-[[sat-solver]]
-== SAT solver
-
-By default Kodkod in ProB uses the bundled SAT4J solver. You can switch
-to using minisat by putting a current version of `libminisat.jnilib`
-into ProB's `lib` directory.
-
-Similarly, as of ProB 1.6.1-beta5 you can also use the Solver
-http://fmv.jku.at/lingeling/[lingeling] or
-http://www.labri.fr/perso/lsimon/glucose/[glucose] by dropping
-`liblingeling.dylib` or `libglucose.dylib` into ProB's lib folder (for
-Mac OS X; for Linux the extension will be different). You can control
-the solver being used using the `KODKOD_SAT_SOLVER` preference (which
-has four possible values: sat4j, minisat, lingeling, glucose).
-
-These files can be downloaded from the
-http://alloy.mit.edu/kodkod/download.html[Kodkod download site].
-
-[[more-preferences]]
-== More Preferences
-
-If you set `KODKOD_ONLY_FULL` to `FALSE`, then the Kodkod translation
-can be applied to part of a predicate. In other words, the predicate
-(such as the PROPERTIES) are partitioned into two parts: one that can be
-understood by Kodkod and the rest which will be dealt with by ProB's
-solver.
-
-You can also enable symmetry by using the preference `KODKOD_SYMMETRY`.
-By default, ProB will set this value to 0, i.e., symmetry is off. This
-means that Kodkod can also be used within set comprehensions. By setting
-the preference to a value higher than 0 you will enable symmetry within
-Kodkod, which may mean that not all solutions will be returned. Setting
-the value too high may be counter productive; Kodkod's recommended
-default is 20.
-
-Finally, you can control the number of solutions that Kodkod computes in
-one go using the preference `KODKOD_MAX_NR_SOLS`. E.g., if you are
-interested in only one solution and `KODKOD_ONLY_FULL` is `TRUE`, then
-you should set this value to 1.
-
-[[more-details-on-kodkod]]
-== More details
-
-* https://www3.hhu.de/stups/downloads/pdf/PlaggeLeuschel_Kodkod2012.pdf[Plagge,
-Leuschel. Validating B, Z and TLA+ using ProB and Kodkod. In Proceedings
-FM'2012, Dimitra Giannakopoulou and Dominique Méry, LNCS 7436, Springer,
-372--386, 2012. (pdf)]
-
-You can also have a look at these Wiki pages:
-
-* <<proving-theorems-in-the-prob-repl,Proving_Theorems_in_the_ProB_REPL>>
-* <<argumentation-theory,Argumentation Theory Example>>
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Z3.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Z3.adoc
deleted file mode 100644
index 4c663296a83e1b0b761e711adca4002fe4f387bf..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Z3.adoc
+++ /dev/null
@@ -1,118 +0,0 @@
-
-[[using-prob-with-z3]]
-= Using ProB with Z3
-
-The current nightly versions of ProB can make use of
-https://github.com/Z3Prover/z3[Z3] as an alternate way of solving
-constraints.
-
-[[how-to-use-z3-within-prob]]
-== How to use Z3 within ProB
-
-One can start a REPL (Read-Eval-Print-Loop) by starting probcli with the
-`-repl` command line option. Any predicate preceded with `:z3` will be
-solved by Z3. The full integration of Z3 and ProB’s kernel can be
-enabled by setting the corresponding preference by passing
-
-`-p SMT SUPPORTED INTERPRETER TRUE`
-
-on the command line.
-
-[[how-to-install-z3-for-prob]]
-== How to install Z3 for ProB
-
-First of all, download a nightly build of ProB from the
-<<download,Downloads>> page. To connect Z3 to ProB you also need the
-proper extension. For Linux and Mac OS, the extension is build by on our
-infrastructure and ships with the regular ProB download. For Windows,
-you can download it from the following URLs:
-
-* https://www3.hhu.de/stups/downloads/z3interface/windows32/z3interface.dll[32bit]
-* https://www3.hhu.de/stups/downloads/z3interface/windows64/z3interface.dll[64bit]
-
-and place it in the "lib" folder of the ProB nightly build.
-
-In addition to ProB, you need to install Z3 by downloading it from
-https://github.com/Z3Prover[Z3's GitHub page]. Currently, ProB is linked
-against the stable release 4.4.1 of Z3. Inside the zip file you will
-find a folder called "bin" with the z3 binary and the belonging
-libraries inside.
-
-These libraries have to be made available to ProB. On Linux or Mac, this
-can either be done by placing them in an appropriate folder (like
-/usr/lib or /usr/local/lib) or by setting an environmental variable
-(like LD_LIBRARY_PATH on Linux or DYLD_LIBRARY_PATH on Mac). On Windows,
-you can place z3.dll in the main folder of the ProB distribution, i. e.,
-on the same level as the lib directory, not inside it. If the libraries
-can not be loaded, ProB will answer with "solver_not_available" when
-Z3 is queried.
-
-[[what-can-be-translated-z3]]
-== What can be translated
-
-Currently, the Z3 translation is unable to cope with the following
-constructs:
-
-* Strings
-* Generalised union, generalised intersection
-* Generalised concatenation
-* Permutation
-* Iteration and Closure
-* Projection
-
-When using Z3 alone, the solver will report
-"unsupported_type_or_expression" if it can not handle parts of a
-constraint.
-
-When used together with ProB, everything Z3 can not be coped with will
-be handled by ProB alone automatically.
-
-[[examples-z3]]
-== Examples
-
-Using the repl, one can try out different examples.
-
-First an example which can be solved by Z3 and not by ProB:
-
-....
->>> X0)
-### Warning: enumerating X : INTEGER : inf:sup ---> -1:3
-Existentially Quantified Predicate over X,Y is UNKNOWN
-[FALSE with ** ENUMERATION WARNING **]
-....
-
-Using the Z3 translation it can be solved:
-
-....
->>> :z3 X>> (2|->4):{y|#x.(y=(x|->x+2))}
-PREDICATE is TRUE
-....
-
-This one cannot be solved by Z3:
-
-....
->>> :z3 (2|->4):{y|#x.(y=(x|->x+2))}
-PREDICATE is UNKNOWN: solver_answered_unknown
-....
-
-Here an example that shows that Z3 can be used to solve constraints and
-obtain solutions for the open variables:
-
-....
->>> :z3 {x} /\ {y} /= {} & x:1000000..20000000 & y>=0 & y<2000000
-PREDICATE is TRUE
-Solution:
-x = 1000000
-y = 1000000
-....
-
-[[more-details-z3]]
-=== More details
-
-A paper describing the integration of ProB and Z3 has been submitted to
-iFM 2016. You can download the
-
-* https://www3.hhu.de/stups/downloads/z3interface/rawdata[raw data] from
-our benchmarks including the R scripts to generate the
-* https://www3.hhu.de/stups/downloads/z3interface/output[resulting
-graphs].
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/ZZ_section_footer.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/ZZ_section_footer.adoc
deleted file mode 100644
index 909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/ZZ_section_footer.adoc
+++ /dev/null
@@ -1,2 +0,0 @@
-
-:leveloffset: -1
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/ZZ_section_footer.adoc b/src/docs/chapter/user/40_AdvancedFeatures/ZZ_section_footer.adoc
deleted file mode 100644
index 909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/40_AdvancedFeatures/ZZ_section_footer.adoc
+++ /dev/null
@@ -1,2 +0,0 @@
-
-:leveloffset: -1