diff --git a/src/docs/asciidoc/chapter/Java_API/05_probcore.adoc b/src/docs/asciidoc/chapter/Java_API/05_probcore.adoc
index 94167695dce63cfd05e61f1eef799b5421659312..9f4a43783ae0c322b1f131e6d8ee9c939cdb0217 100644
--- a/src/docs/asciidoc/chapter/Java_API/05_probcore.adoc
+++ b/src/docs/asciidoc/chapter/Java_API/05_probcore.adoc
@@ -2,14 +2,14 @@
 [[developer-high-level-api]]
 = High Level API
 
-We have introduced a high level API in ProB 2.0 which allows much nicer interaction with ProB. Before 2.0, all interaction was done using commands. There were no abstractions that represent typically used concepts such as a model, a state space, or a trace. Together with this high level API, we introduced a scripting interface that makes it very easy to tweak ProB and implement new features. Almost everything in ProB can be manipulated through Groovy scripts. This chapter will introduce the programmatic abstractions now available in ProB 2.0, and will briefly describe their function. Later chapters will cover in greater depth how to use the abstractions. <<animation>> covers the topic of animation, and <<evaluation>> discusses how to evaluate formulas using the API. In the following sections we will introduce the main abstractions that are available in ProB 2.0, that is, the model, state space and trace abstractions.
+We have introduced a high level API in ProB 2.0 which allows much nicer interaction with ProB. Before 2.0, all interaction was done using commands. There were no abstractions that represent typically used concepts such as a model, a state space, or a trace. Together with this high level API, we introduced a scripting interface that makes it very easy to tweak ProB and implement new features. Almost everything in ProB can be manipulated through Groovy scripts. This chapter will introduce the programmatic abstractions now available in ProB 2.0, and will briefly describe their function. Later chapters will cover in greater depth how to use the abstractions. <<developer-animation>> covers the topic of animation, and <<developer-evaluation-and-constraint-solving>> discusses how to evaluate formulas using the API. In the following sections we will introduce the main abstractions that are available in ProB 2.0, that is, the model, state space and trace abstractions.
 
 == Experimenting with ProB 2.0
 The best way to get a feel for ProB 2.0 is to try it out in a Groovy environment. Within the GUI, a Groovy shell can be opened from the _Advanced_ menu.
 
 ProB will automatically provide some predefined objects for interaction in Groovy shells. The most interesting predefined objects are stored in the `api` and `animations` variables.
 
-The next section will only contain examples referencing the `api` variable, a singleton instance of the `Api` class, which has methods to load models for a number of different formalisms (currently classical B, Event-B, TLA+ and CSP). The `animations` variable is used to programatically interact with the user interface and will be referenced frequently in <<animation>>.
+The next section will only contain examples referencing the `api` variable, a singleton instance of the `Api` class, which has methods to load models for a number of different formalisms (currently classical B, Event-B, TLA+ and CSP). The `animations` variable is used to programatically interact with the user interface and will be referenced frequently in <<developer-animation>>.
 
 == Model Abstraction
 The model abstraction provides static information about the current model that is being animated or checked. For Classical B and Event-B, this includes all of the information about the refinement chain and all of the different components (Machines, Contexts, Invariants, Variables, etc.). Currently, the model abstraction has been implemented for the Classical B, Event B, TLA+ and CSP-M formalisms. However, because we have implemented the abstraction with other formalisms in mind, it is not difficult to implement new formalisms.
@@ -92,11 +92,11 @@ public abstract class AbstractModel extends AbstractElement {
 
 When extracting the model from a specification file, the main component is usually inherently specified. The user will extract the component `/path/to/dir/spec1.mch` and will expect that the component with the name `spec1` will have been loaded. For this reason, we have introduced the `ExtractedModel` abstraction.
 
-We have abstracted the loading mechanism for specifications so that it can be adapted to load any number of different formalisms. The classes responsible for loading the models basically have to perform three tasks: extract the static information about the specification in question, create a command to load the model into the Prolog kernel, and subscribe any formulas of interest (the subscription mechanism will be explained more in <<evaluation>>. The load command consists of setting user specified preferences, a formalism specific load command for the model, and a request for ProB to start animating the model in question. Each formalism that is supported by ProB has its own factory responsible for loading it. These factories can be created via <<dependency_injection>>, and they also have accessor methods in the `Api` class which makes it simple to load specifications in a groovy environment.
+We have abstracted the loading mechanism for specifications so that it can be adapted to load any number of different formalisms. The classes responsible for loading the models basically have to perform three tasks: extract the static information about the specification in question, create a command to load the model into the Prolog kernel, and subscribe any formulas of interest (the subscription mechanism will be explained more in <<developer-evaluation-and-constraint-solving>>. The load command consists of setting user specified preferences, a formalism specific load command for the model, and a request for ProB to start animating the model in question. Each formalism that is supported by ProB has its own factory responsible for loading it. These factories can be created via <<dependency-injection>>, and they also have accessor methods in the `Api` class which makes it simple to load specifications in a groovy environment.
 
 The load method of a factory takes three parameters:
 * the `String` path to the specification file
-*  a `Map<String,String>` of user specified preferences (for list of possible preferences see <<preferences>>)
+*  a `Map<String,String>` of user specified preferences (for list of possible preferences see https://prob.hhu.de/w/index.php/Using_the_Command-Line_Version_of_ProB#Preferences[the ProB wiki])
 * a Groovy closure (the Groovy implementation of a lambda function) that takes the loaded model as a parameter and will execute user defined behavior
 
 == Load Function
@@ -112,7 +112,7 @@ loadClosure = { model ->
 
 Of course, this particular closure may not be useful for the user, but adding this functionality allows users to define actions that need to be taken directly after the model has been loaded. It is also possible to simply use an empty closure that does nothing. For those programming a Java environment, a predefined empty closure is defined as `Api.EMPTY`.
 
-When loading the model into the user interface, we want formulas of interest to tell the state space to evaluate themselves in every step of the animation so that their values can be cached and easily retrieved. This evaluation mechanism is described further in <<evaluation>>. To do this, we have implemented the `Api.DEFAULT` closure which will tell ProB that all invariants, variables, and constants are of interest.
+When loading the model into the user interface, we want formulas of interest to tell the state space to evaluate themselves in every step of the animation so that their values can be cached and easily retrieved. This evaluation mechanism is described further in <<developer-evaluation-and-constraint-solving>>. To do this, we have implemented the `Api.DEFAULT` closure which will tell ProB that all invariants, variables, and constants are of interest.
 
 As mentioned before, the model factories (`ClassicalBFactory`, `EventBFactory`, `CSPFactory`, and `TLAFactory`) can be retrieved from the injector framework. However, there are also methods for loading the specifications in the `Api` class to allow access from a Groovy environment. The next sections will briefly cover how to load different specifications and the special characteristics for the specification in question. Each of the load methods in the `Api` take three parameters, but there are also default values for the parameters that are supplied if the user does not choose to define one of them. To take the optional parameters into account, groovy compiles a single method call into three separate method calls as shown in the following:
 
@@ -282,7 +282,7 @@ println transition.getRep()  // pretty print of the transition
 
 When using transitions, however, it is important to be aware that not all of these fields are filled by default. The source and destination states, the id, and the name are all defined, but the parameters and return values are retrieved lazily only if they are needed. This is because many specifications written in classical B or Event-B have very large parameter values, and these parameter values need to be sent from the prolog side to the Java side. Because the communication between the two uses sockets and the parsing of strings, having to send large strings results in a visible performance decrease. Often, the user doesn't need to use the parameter values, so it made sense to retrieve them lazily from Prolog.
 
-However, even retrieving the parameters and return values at a later time can be inefficient if you are dealing with multiple transitions for which you need to retrieve the parameters at the same time. For this reason, we have made the `evaluateTransitions` method in the state space, which takes a collection of transitions and retrieves their parameters and return values in one go by composing the requests to Prolog into one query as described in <<lowlevel>>. This results in better performance because for a list of transitions with n elements, only one communication step is required instead of n steps.
+However, even retrieving the parameters and return values at a later time can be inefficient if you are dealing with multiple transitions for which you need to retrieve the parameters at the same time. For this reason, we have made the `evaluateTransitions` method in the state space, which takes a collection of transitions and retrieves their parameters and return values in one go by composing the requests to Prolog into one query as described in <<developer-low-level-api>>. This results in better performance because for a list of transitions with n elements, only one communication step is required instead of n steps.
 
 In addition to the `evaluateTransition` method, we have also modified the getter methods for classes containing lists of transitions (i.e. the `getOutTransitions` method in the State class and the `getTransitionList` and `getNextTransitions` method in the `Trace` class). S
 
diff --git a/src/docs/asciidoc/prob_handbook.adoc b/src/docs/asciidoc/prob_handbook.adoc
index 522ecdf4fc4d20c9aeacdbc9799897840e524667..012b7cf669665e2e3cfb73bd98f0a12cad9bbff0 100644
--- a/src/docs/asciidoc/prob_handbook.adoc
+++ b/src/docs/asciidoc/prob_handbook.adoc
@@ -23,12 +23,11 @@ are available.
 [[important-notice]]
 == Important notice
 
-If you find a problem with ProB or this documentation please let us
-know. We are happy to receive suggestions for improvements to ProB or
-the documentation. More information about submitting bug reports is
-available in the <<bugs,bugs section>>. You can also post
-a question in our https://groups.google.com/d/forum/prob-users[prob-users group] or send
-an email to mailto:Michael.Leuschel@hhu.de[Michael Leuschel].
+If you find a problem with ProB or this documentation please let us know.
+We are happy to receive suggestions for improvements to ProB or the documentation.
+You can submit bug reports on our https://github.com/hhu-stups/prob-issues/issues[issue tracker].
+You can also post a question in our https://groups.google.com/d/forum/prob-users[prob-users group]
+or send an email to mailto:Michael.Leuschel@hhu.de[Michael Leuschel].
 
 [[developer-prob-java-api]]
 = ProB 2.0 Java API Documentation