diff --git a/src/docs/chapter/user/70_TclTk/00_section_header.adoc b/src/docs/chapter/user/70_TclTk/00_section_header.adoc
deleted file mode 100644
index c68e1ae467eca1deb650d654d0f74563412f8bac..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/70_TclTk/00_section_header.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-
-[[tcltk]]
-= Tcl/Tk
-:leveloffset: +1
diff --git a/src/docs/chapter/user/70_TclTk/Tk_Architecture.adoc b/src/docs/chapter/user/70_TclTk/Tk_Architecture.adoc
deleted file mode 100644
index 70ab1d2ca6e0bc1177aec92edf91898a170ab7a4..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/70_TclTk/Tk_Architecture.adoc
+++ /dev/null
@@ -1,104 +0,0 @@
-
-[[theprob-tcltk-cross-language-architecture]]
-= The ProB Tcl/Tk cross-language architecture
-
-The ProB Tcl/Tk contains a mixture of Prolog and Tcl/Tk source code. The
-core (i.e., the constraint solver, the animation engine, the model
-checker, ...) are all written in Prolog (which in turn may call some C
-external functions, e.g., for LTL model checking).
-
-We use the SICStus library(tcltk) (see chapter 10.40 of SICStus manual)
-
-Overall, the communication works as follows:
-
-* on startup ProB launches Tcl/Tk; most of the GUI code can be found
-inside `main_prob_tcltk_gui.tcl`
-* from then on Tcl/Tk controls the GUI and calls Prolog predicates
-* Tcl/Tk code calls Prolog using `prolog PRED(…X…Y…)`
-* Tcl/Tk then gets result values using `$prolog_variables(X)` or
-`$prolog_variables(Y)`. There are only limited Prolog datatypes that can
-be transferred from Prolog to Tcl/Tk in this way; see below.
-* Tcl/Tk code can also check if a Prolog call was successful, e.g.:
-`if [prolog tcltk_backtrack] { … }`
-* Tcl/Tk code usually calls predicates with tcltk in their name; but
-there are exception (evaluation_view.tcl calls bvisual2 predicates)
-
-The library(tcltk) puts restrictions on what can be transferred from
-Prolog to Tcl/Tk and then extracted using `$prolog_variables(VAR)`:
-
-* integer
-* atoms (which get translated to Tcl strings)
-* lists of integer or atoms
-* nested lists of the above; in this case the Prolog code should not
-return the list but wrap the list result inside a `list(.)` constructor
-
-[[how-to-add-a-simple-menu-command]]
-== How to add a simple menu command
-
-You need to add an entry in the ProB Tcl/Tk menu. The menus are defined
-at the top of the file `main_prob_tcltk_gui.tcl`
-
-....
-.frmMenu.mnuAnalyse.mnuCoverage add command -label "Number of Values for all Variables" -command {procNrVariableValuesOverStatespace}
-....
-
-You also need to define the Tcl/Tk part of your command (probably inside `main_prob_tcltk_gui.tcl`):
-
-....
-proc procNrVariableValuesOverStatespace {}
-    if [prolog “tcltk_compute_nr_covered_values_for_all_variables(Res)"] {
-        procShowErrors
-        procShowTable $prolog_variables(Res) "Coverage Table" "Number of Covered Values for Variables" "CoverageVariablesTable" "" ""
-    } else {
-        procShowErrors
-    }
-}
-....
-
-Observe the use of `prolog` to call Prolog predicates and
-`$prolog_variables` to extract return values obtained from Prolog (which
-should instantiate the corresponding variable/argument). Also observer
-that we call `procShowErrors`, a Tcl/Tk procedure, which extracts all
-pending error messages and displays them to the user. procShowTable is a
-utility to display a dialog box containing a table.
-
-Finally, we need to define the called Prolog predicate somewhere in the
-Prolog code:
-
-....
-tcltk_compute_nr_covered_values_for_all_variables(list([list(['Variable', 'Number of Values'])|VL])) :-
-    state_space:get_state_space_stats(NrNodes,_,_),
-    format('Computing all values in ~w states for all variables~n',[NrNodes]),
-    findall(list([ID,Count]),number_of_values_for_variable(ID,Count),VL),
-    format('Finished computing all values for all variables~n',[]).
-....
-
-The use of format is more for debugging (the output will not be seen by
-ProB Tcl/Tk, just on the console (if any) used to launch ProB Tcl/Tk).
-
-The command is now available and ready to use:
-
-image::ProB_TclTk_CountVarMenu.png[]
-
-[[some-useful-prob-tcltk-procedures]]
-== Some useful ProB Tcl/Tk procedures
-
-* procShowErrors: collect all new errors and warnings from the Prolog
-error_manager and displays them in a dialog (in batch mode they are
-printed on the console only)
-* procShowList, procShowTable: pops up dialog boxes to display lists or
-tables (lists of lists). Parameters are title of dialog box,…
-* procInsertHistoryOptionsState: updates the State, History and
-Operations (Options) views by calling Prolog and getting information
-about the current state
-
-NOTE: The Tcl/Tk code is mostly state-less, almost everything is stored
-inside Prolog:
-
-* current animation state
-* animation history and forward history
-* state space (all visited states and transitions)
-* all errors that have occurred (stored by the error_manager.pl)
-* the current specification
-* the state of all the preferences (inside preferences.pl)
-* ...
diff --git a/src/docs/chapter/user/70_TclTk/ZZ_section_footer.adoc b/src/docs/chapter/user/70_TclTk/ZZ_section_footer.adoc
deleted file mode 100644
index 909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/70_TclTk/ZZ_section_footer.adoc
+++ /dev/null
@@ -1,2 +0,0 @@
-
-:leveloffset: -1