diff --git a/src/docs/chapter/user/60_JavaAPI/00_section_header.adoc b/src/docs/chapter/user/60_JavaAPI/00_section_header.adoc
deleted file mode 100644
index 43a534483239e121953e8dd23ca590c772958d8d..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/60_JavaAPI/00_section_header.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-
-[[prob2-java-api]]
-= ProB 2.0 Java API
-:leveloffset: +1
diff --git a/src/docs/chapter/user/60_JavaAPI/01_ProB_Java_API.adoc b/src/docs/chapter/user/60_JavaAPI/01_ProB_Java_API.adoc
deleted file mode 100644
index f8d4e56fe4e4b8cb6eaa02d5d99f95ad52af0366..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/60_JavaAPI/01_ProB_Java_API.adoc
+++ /dev/null
@@ -1,33 +0,0 @@
-
-[[general-java-api]]
-= General
-
-[[prob-java-api-documentation]]
-== Documentation
-
-* <<prob-java-api-tutorial,Tutorial>>
-
-* <<developer-introduction, Documentation>>
-== Additional Material
-
-* <<prob2.0-development,ProB 2.0 Development>>
-* https://github.com/bendisposto/prob2_tooling_template[ProB 2.0 Tooling
-Template]
-* <<programmatic-abstractions-in-prob-api,Programmatic_Abstractions_in_the_ProB_2.0_API>>
-* https://docs.google.com/document/pub?id=109z3qG6_KBUqm0NC9FaEF1C6_NYCJl453wcXzbovj2Q[ProB
-2.0 Requirements Document] +
-(if you want to comment on the Document, please use goo.gl/KS2bh)
-
-* <<user-and-developer-workshop,Rodin User and Developer Workshop 2013 -
-Tutorial Presentation>>
-
-* <<tutorial13,Rodin User and Developer Workshop 2013 - Tutorial>>
-
-* <<prob-2.0-within-rodin-and-a-html-visualization-example,ProB 2.0
-within Rodin and a HTML Visualization Example>>
-
-== Download
-
-Nightly builds of ProB 2 for Rodin 3 can be obtained from within Rodin
-using the update site
-http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/nightly/[http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/nightly/].
diff --git a/src/docs/chapter/user/60_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc b/src/docs/chapter/user/60_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc
deleted file mode 100644
index fcca19257dc86b0d78c16502319f7026a90e6b9d..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/60_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc
+++ /dev/null
@@ -1,86 +0,0 @@
-
-[[programmatic-abstractions-in-prob-api]]
-= Programmatic Abstraction in the ProB 2.0 API
-
-[[overview-programmatic-abstractions-in-prob-api]]
-== Overview
-
-[[background]]
-=== Background
-
-The original ProB plug-in for Rodin introduced one basic abstraction:
-developers can create Java commands specifying calculations that are to
-be made by the ProB CLI binary. The result that is calculated by ProB
-can then be interpreted and manipulated by the developer. Each Java
-command corresponds to one prolog instruction in the ProB kernel.
-
-[[current-implementation]]
-=== Current Implementation
-
-We have maintained the abstractions of the commands in order to
-communicate with the ProB kernel. However, as we were considering how
-the ProB core should be structured, we realized that many commands may
-be used over and over again in the same (or very similar) concepts.
-Therefore, we created the programmatic abstractions that will be
-described in the following sections.
-
-[[java-api-model]]
-== Model
-
-The Model is an abstraction that 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.).
-
-This abstraction is available so that it is possible to have access to
-the static information about the model during an animation without
-having to contact ProB directly.
-
-Currently, the Model abstraction is implemented for the Classical B and
-Event B formalisms. But because we have implemented the abstraction with
-other formalisms in mind, it should not be difficult to implement new
-formalisms. We have also implemented a Model abstraction for CSP-M
-specifications, but it is currently not possible to access any static
-information about the model. TLA+ specifications can be represented in
-the API as Classical B models.
-
-[[java-api-statespace]]
-== StateSpace
-
-There is a one-to-one relationship between a StateSpace and a model. The
-StateSpace is the corresponding label transition system for a particular
-model.
-
-Conceptually, the state space is completely there and completely
-evaluated. When you access a state within the StateSpace, ProB will
-fetch the information from Prolog automatically and transparently. The
-only observation that can be made is that the fetching of some states
-takes longer than the ones that are already "cached" in the
-StateSpace. For performance reasons, not all states in the state space
-are saved indefinitely. The states in the StateSpace are saved as State
-objects, which then hold the information about the outgoing transitions
-and formulas of interest that have been evaluated for the given state.
-In the StateSpace, these objects are cached in an LRU cache so that if
-not accessed for a given period of time, the garbage collector can clean
-them up.
-
-[[java-api-trace]]
-== Trace
-
-For some tools, the StateSpace abstraction may be sufficient. But when
-it comes to animation and the concept of a "current state", a further
-abstraction becomes necessary. The Trace provides this abstraction.
-
-A Trace consists of a linked list of states which correspond to a path
-through the StateSpace. There is also a pointer in the list which
-identifies the current state. The Trace behaves like a browser history;
-it is possible to move forward and backward within the current trace.
-
-A Trace corresponds to exactly one trace within the animation. Each
-Trace is associated with exactly one StateSpace, but we can have many
-different Trace objects on top of a single StateSpace.
-
-The Trace is immutable. This means that whenever an animation step is
-performed (forward, backward, or simply adding a transition to the
-trace) a new Trace is returned.
diff --git a/src/docs/chapter/user/60_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc b/src/docs/chapter/user/60_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc
deleted file mode 100644
index 9ac986f3d215418c2c3df619fd8d9cbe90ab7c59..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/60_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc
+++ /dev/null
@@ -1,388 +0,0 @@
-
-[[rodin-user-and-developer-workshop-2013]]
-= Rodin User and Developer Workshop 2013
-
-Here are the information we have shown you at the tutorial. If you want
-to follow this tutorial on your computer you will have to install ProB
-2.0 and start an animation. For this tutorial we use a
- image::Scheduler_tutorial2013.zip[]. Maybe you
-have to clean the project after importing.
-
-This page was updated in May of 2015 to reflect changes made to the ProB
-2.0 API.
-
-[[java-api-setup]]
-== Setup
-
-You will need a fresh copy of ProB 2.0 installed to your Rodin or the
-sourcecode.
-
-The update site for our builds is:
-http://nightly.cobra.cs.uni-duesseldorf.de/experimental/updatesite/
-
-The sourcecode repository and a description how to setup your Eclipse:
-https://github.com/bendisposto/prob2
-
-Please note that no matter which installation method you chose, you need
-to fetch the latest Prolog binaries. The easiest way is to type
-'upgrade "latest"` into the ProB 2.0 Groovy console.
-
-In the following we will intermix some explanations with FAQ style code
-snippets. We assume that you execute all the code snippets. Some of the
-snippets rely on the previous execution of other snippets.
-
-[[java-api-preparation]]
-== Preparation
-
-1.  Import the Scheduler project.
-2.  Start an animation for Scheduler0
-3.  Perform some random animation steps
-4.  Type `trace = animations.getCurrentTrace()` into the Groovy console.
-This accesses the current animation and saves it in the `trace`
-variable.
-5.  Type `s = trace.getStateSpace()` to save a reference to the state
-space that is associated with `trace`
-
-[[java-api-the-model]]
-== The Model
-
-A model gives you access to the static properties of a Rodin
-development. Such as contexts, machines, constants, variables,
-invariants, events, etc. A model is a graph of components and their
-relationship. Except for Graph handling there are no shared methods
-between formalisms. The main difference between EventBModel and
-ClassicalBModel are the artifacts and relationships they can contain. An
-EventB Model consists of Machines and Contexts and the only
-relationships are refinement and sees.
-
-*How can we get the model for a given state space?*
-
-`m = s.getModel()`
-
-*What is the Java type of m?*
-
-`m.getClass()`
-
-An EventB model consists of machines and contexts. Machines allow to
-access variables, invariants, variants and events. Contexts give you
-access to axioms, constants and sets. Let's explore machines.
-
-*How do we get access to the Scheduler0 machine?*
-
-`mch = m.getComponent("Scheduler0")`
-
-*What are the invariants of Scheduler0?*
-
-`mch.getInvariants()`
-
-*What are the events of Scheduler0?*
-
-`mch.getEvents()`
-
-*How can we access the event named new?*
-
-`ne = mch.getEvent("new")`
-
-*What is the guard of new?*
-
-`ne.getGuards()`
-
-[[java-api-the-state-space]]
-== The State Space
-
-
-The state space represents the whole currently known world for an
-animation. It is lazily explored. Information about the state space is
-stored in State objects which can be queried to inspect information
-about any given state. These State objects are cached and can be
-accessed via their string identifier.
-
-*How do we retrieve the state space for a given model?*
-
-`s = m.getStateSpace()`
-
-In Rodin, you should try to explore the state until your trace contains
-the `massakr` event. This event breaks the invariant of the system.
-Otherwise the next command will return an empty set.
-
-*How can I access the current state from an animation?*
-
-`state = trace.getCurrentState()`
-
-*Does the state that violate the invariant?*
-
-`state.getInvariantOk()`
-
-*Can we get the value of a variable in that state?*
-
-`state.eval("active")`
-
-*Can we randomly "execute" events?*
-
-`y = state.anyEvent()`
-
-*Can we "execute" a specific event?*
-
-Yes we can! We will figure out how it is done in a moment.
-
-*How do we find out which events are enabled?*
-
-`state.getOutTransitions()`
-
-*What are the elements of this list?*
-
-`state.getOutTransitions().first().getClass()`
-
-*Now let's get one of these Transition objects*
-
-`trans = state.getOutTransitions()[1]`
-
-*What is the name of the transition?*
-
-`n = trans.getName()`
-
-*What are the actual parameters?*
-
-`params = trans.getParams()`
-
-*What is the formal parameter name?*
-
-`e = mch.getEvent(trans.getName())`
-
-Finally we can "execute" the Event using the perform method of the
-StateId object. At this point you need to chose an event that you want
-to execute. It has to be enabled in the state, but you can provide
-additional guards to restrict the parameters. For instance if the event
-del is enabled and we want to delete process P2 the command is
-
-*state.perform("del",["r=P2"])*
-
-We try not to intertwine different aspects of the system. That is why we
-had to get the formal parameter from the model's representation, the
-enabled operations from the state, and the detail information from the
-Transition object. This design principle was taken from Rich Hickey's
-http://www.infoq.com/presentations/Simple-Made-Easy[Simple made easy]
-talk.
-
-However, this doesn't prevent us (or you!) from adding convenience
-functions!
-
-*How do I execute an event?*
-
-....
-def exec(mch,state,name,params) {
-  formal_params = mch.getEvent(name).getParameters()
-  pred = [formal_params,params].transpose()
-   .collect { a,b -> a.toString() + "=" + b.toString() }
-  state.perform(name,pred)
-}
-....
-
-You can write your own set of convenience functions in a groovy file and
-run it at the beginning.
-
-`run new File("myAwesomeScript.groovy")`
-
-[[java-api-traces]]
-== Traces
-
-A trace represents a path through the state space. It can move forward
-and backward through the Trace and can be extended with a new
-transition. Traces are immutable, yet creating new traces is efficient
-because of structural sharing.
-
-*How can we track a trace of events?*
-
-`t = new Trace(s)`
-
-*What is the current state of the trace?*
-
-`t.getCurrentState()`
-
-*What are the enabled events in the current state?*
-
-`t.getNextTransitions()`
-
-*How can we "execute" an event?*
-
-`t = t.add(t.getNextTransitions().first())`
-
-*How can we produce a random trace?*
-
-`def randTrace(t,n) {` +
-`  def nt = t;` +
-`  n.times {  nt = nt.anyEvent() }` +
-`  nt` +
-`}`
-
-*Let's run it!*
-
-`randTrace(t,20)`
-
-'''How can go back in time? '''
-
-`t = t.back()`
-
-*How can we go forward in time?*
-
-`t = t.forward()`
-
-If we go back in time, the trace keeps future states. If we change a
-decision in the past, the trace drops the future. It behaves in the same
-way your browser history does.
-
-[[java-api-evaluation]]
-== Evaluation
-
-Evaluation is done by passing an instance of the interface IEvalElement
-to an evaluator. Each formalism has its own descendant of IEvalElement.
-They apply a parser to a String
-
-*How can we create an EventB formula?*
-
-`f1 = "active \\/ waiting"` as EventB
-
-The escaping of the backslash is unfortunatly required because the
-formula is contained in a Java String.
-
-*And how do we create a classical B formula?*
-
-`f2 = "active \\/ waiting"` as ClassicalB
-
-*How can we evaluate the formulas for state x?*
-
-`x.eval(f1)`
-
-*What have we received?*
-
-`x.eval(f1).getClass()`
-
-ProB's Prolog engine does not make a difference between EventB and
-classical B. Only the parsers are different. Event B Formulas are parsed
-by Rodin. Classical B formulas are parsed by ProB's parser.
-
-*Ok, we can evaluate a formula for a state. Anything else that evaluates
-formulas?*
-
-`t.eval(f1)`
-
-Traces evaluate a formula for each state of the trace. They return a
-list of results.
-
-*Anything else?*
-
-`s.evaluateForGivenStates(t.getTransitionList().collect { it.getSource()},[f1, "waiting" as EventB])`
-
-evaluateForGivenStates takes a list of states and a list of formulas and
-evaluates them for each state of the statespace. This method is not
-called eval to prevent accidental evaluation.
-
-*Can we evaluate the guard of an event for a whole trace?*
-
-....
-g = mch.getEvent("del").getGuards()
-g = g.collect {it.toString()}.join(" & ")
-t.eval(g)
-....
-
-`"I want to have it extra sweet!"`
-
-....
-String.metaClass.and = {b -> "("+delegate+") & ("+b + ")" }
-not = { "not("+it+")" }
-String.metaClass.implies = {b -> "("+delegate +") => (" + b + ") "}
-conj = { it.collect{it.toString()}.inject {a,b -> a & b}}
-....
-
-This piece of code introduces four functions to simplify handling of
-formulas. The first line overrides the & operator for Strings and allows
-us to conjoin two predicates as Strings, e.g., `"1<4" & "x>y"`
-evaluates to `"(1<4) & (x>y)"`. The second line implements a
-function not that wraps a predicate into a negation. The third line adds
-an implies method to the class String. `"1<2".implies("3<4")`
-results in `"(1<2) => (3<4)"`. The last line converts a list
-of predicates into a conjunction. In Groovy collect means map and inject
-means reduce.
-
-[[java-api-constraint-solver]]
-== Constraint solver
-
-*Evaluation is fine, but can I use ProB's solver?*
-
-....
-f4 = new EventB("a = 1 & b = a - 1")
-c4 = new CbcSolveCommand(f4)
-s.execute(c4)
-c4.getValue()
-....
-
-The state space in the example has two purposes. It is used to tell the
-typechecker which constants and sets exist in the model. It also allows
-us to send commands to the Prolog core of ProB.
-
-'''What do we get if the predicate is not solvable? '''
-
-....
-f4 = new ClassicalB("a = a - 1")
-c4 = new CbcSolveCommand(f4)
-s.execute(c4)
-c4.getValue()
-....
-
-*Can we get rid of that Java stuff please?*
-
-....
-def cbc_solve(space, formula) {
-  e = new EventB(formula)
-  c = new CbcSolveCommand(e)
-  space.execute(c)
-  c.getValue()
-}
-....
-
-*Can we find out if one event can in principle be enabled, i.e., it is
-not dead code?*
-
-....
-i = conj(mch.getInvariants())
-g = conj(mch.getEvent("del").getGuards())
-cbc_solve(s, i & i.implies(g))
-....
-
-[[java-api-notification-and-ui-access]]
-== Notification and UI Access
-
-Clients can register themself to receive a notification if an animation
-step occured, new states were discovered or the model has changed. The
-client has to implement one of the Listener interfaces from the
-de.prob.statespace package.
-
-ProB 2.0 was built on top of the same commands as ProB 1.0. Most of the
-commands are usable with only minor changes. ProB 2.0 can be extended in
-the same way as ProB 1.0.
-
-To access the user interface, ProB 2.0 injects two special objects into
-the console, `animations` and `api`.
-
-`animations` is an Instance of `AnimationSelector`, `api` is an instance
-of `Api`. The selector maintains lists of Traces and State Spaces. The
-trace shown in the UI is marked as the current trace. The Api object is
-used to load models. Most likely we will rename this class and instance
-in the future to something more meaningful, e.g., loader.
-
-*Can I get the trace that is shown in the UI?*
-
-`animations.getCurrentTrace()`
-
-*What traces are registered?*
-
-`animations.getTraces()`
-
-*Can I add a trace to the UI?*
-
-`animations.addNewAnimation(t)`
-
-[[java-api-additional-resources]]
-== Additional Resources
-
-Further information can be found in the ProB Developer_Manual.
diff --git a/src/docs/chapter/user/60_JavaAPI/ZZ_section_footer.adoc b/src/docs/chapter/user/60_JavaAPI/ZZ_section_footer.adoc
deleted file mode 100644
index 909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/60_JavaAPI/ZZ_section_footer.adoc
+++ /dev/null
@@ -1,2 +0,0 @@
-
-:leveloffset: -1