diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index 494f1567092de90ab5ac3176d564c1fa2bcc569b..c6e1ae6f7cbb1ad503bd335f9d2b0fca239e536d 100644
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -14,13 +14,13 @@
        "\n",
        "Show information about the current state.\n",
        "\n",
-       "The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of transitions that are available in the current state."
+       "The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of enabled operations (and possible parameter values) in the current state."
       ],
       "text/plain": [
        ":browse\n",
        "Show information about the current state.\n",
        "\n",
-       "The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of transitions that are available in the current state."
+       "The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of enabled operations (and possible parameter values) in the current state."
       ]
      },
      "execution_count": 1,
@@ -46,13 +46,17 @@
        "\n",
        "Execute an operation.\n",
        "\n",
-       "A transition for the given operation is found and executed. If the optional predicate is specified, a transition is found for which the predicate is $\\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have."
+       "The predicate is used to select the operation's parameter values. The parameters can be fully specified explicitly (e. g. `:exec op param1 = 123 & param2 = {1, 2}`), or they can be partially constrained (e. g. `:exec op param1 > 100 & card(param2) >= 2`) to let ProB find a valid combination of parameters. If there are multiple valid combinations of parameters that satisfy the predicate, it is undefined which one is selected by ProB.\n",
+       "\n",
+       "If no predicate is specified, the parameters are not constrained, and ProB will select an arbitrary valid combination of parameters."
       ],
       "text/plain": [
        ":exec OPERATION [PREDICATE]\n",
        "Execute an operation.\n",
        "\n",
-       "A transition for the given operation is found and executed. If the optional predicate is specified, a transition is found for which the predicate is $\\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have."
+       "The predicate is used to select the operation's parameter values. The parameters can be fully specified explicitly (e. g. `:exec op param1 = 123 & param2 = {1, 2}`), or they can be partially constrained (e. g. `:exec op param1 > 100 & card(param2) >= 2`) to let ProB find a valid combination of parameters. If there are multiple valid combinations of parameters that satisfy the predicate, it is undefined which one is selected by ProB.\n",
+       "\n",
+       "If no predicate is specified, the parameters are not constrained, and ProB will select an arbitrary valid combination of parameters."
       ]
      },
      "execution_count": 2,
diff --git a/notebooks/tests/assert.ipynb b/notebooks/tests/assert.ipynb
index f2476511aa3c1cc46562ee1ea73aeab5e23de414..8d6f5147887ad8e2aba1137613f0fd4b57dca405 100644
--- a/notebooks/tests/assert.ipynb
+++ b/notebooks/tests/assert.ipynb
@@ -14,17 +14,21 @@
        "\n",
        "Ensure that the predicate is true, and show an error otherwise.\n",
        "\n",
-       "This command is intended for verifying that a predicate is always true at a certain point in a notebook. Unlike normal evaluation (`:eval`), this command treats a $\\mathit{FALSE}$ result as an error. If the result is $\\mathit{TRUE}$, solutions for free variables (if any) are not displayed.\n",
+       "Unlike normal evaluation (`:eval`), this command treats a $\\mathit{FALSE}$ result as an error. If the result is $\\mathit{TRUE}$, solutions for free variables (if any) are not displayed.\n",
        "\n",
-       "Only predicates and $\\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error."
+       "Only predicates and $\\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error.\n",
+       "\n",
+       "This command is intended for verifying that a condition holds at a certain point in the notebook. It may also be used in combination with the Jupyter Notebook [nbgrader](https://nbgrader.readthedocs.io/) extension for automatic checking/grading of exercises."
       ],
       "text/plain": [
        ":assert PREDICATE\n",
        "Ensure that the predicate is true, and show an error otherwise.\n",
        "\n",
-       "This command is intended for verifying that a predicate is always true at a certain point in a notebook. Unlike normal evaluation (`:eval`), this command treats a $\\mathit{FALSE}$ result as an error. If the result is $\\mathit{TRUE}$, solutions for free variables (if any) are not displayed.\n",
+       "Unlike normal evaluation (`:eval`), this command treats a $\\mathit{FALSE}$ result as an error. If the result is $\\mathit{TRUE}$, solutions for free variables (if any) are not displayed.\n",
+       "\n",
+       "Only predicates and $\\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error.\n",
        "\n",
-       "Only predicates and $\\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error."
+       "This command is intended for verifying that a condition holds at a certain point in the notebook. It may also be used in combination with the Jupyter Notebook [nbgrader](https://nbgrader.readthedocs.io/) extension for automatic checking/grading of exercises."
       ]
      },
      "execution_count": 1,
diff --git a/notebooks/tests/eval.ipynb b/notebooks/tests/eval.ipynb
index c1b1ac008e8c5a985af0a28eaa141064d42c5423..6cdfedfcfbace8d6a9aae79c195358447829339f 100644
--- a/notebooks/tests/eval.ipynb
+++ b/notebooks/tests/eval.ipynb
@@ -9,22 +9,26 @@
      "data": {
       "text/markdown": [
        "```\n",
+       "FORMULA\n",
+       "// or\n",
        ":eval FORMULA\n",
        "```\n",
        "\n",
        "Evaluate a formula and display the result.\n",
        "\n",
-       "This is equivalent to inputting the formula without a command name.\n",
+       "Normally you do not need to explicitly call `:eval` to evaluate formulas. If you input a formula without any command before it, it is evaluated automatically (e. g. `:eval 1 + 2` is equivalent to just `1 + 2`).\n",
        "\n",
-       "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed."
+       "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed. For more control about which solver is used to solve the predicate, use the `:solve` command."
       ],
       "text/plain": [
+       "FORMULA\n",
+       "// or\n",
        ":eval FORMULA\n",
        "Evaluate a formula and display the result.\n",
        "\n",
-       "This is equivalent to inputting the formula without a command name.\n",
+       "Normally you do not need to explicitly call `:eval` to evaluate formulas. If you input a formula without any command before it, it is evaluated automatically (e. g. `:eval 1 + 2` is equivalent to just `1 + 2`).\n",
        "\n",
-       "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed."
+       "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed. For more control about which solver is used to solve the predicate, use the `:solve` command."
       ]
      },
      "execution_count": 1,
diff --git a/notebooks/tests/help.ipynb b/notebooks/tests/help.ipynb
index cbcb887c0136e3838cdc367f2ce9fd33f617c14b..fb5e3e3904fe07e47869ea3c58334367214cb9e8 100644
--- a/notebooks/tests/help.ipynb
+++ b/notebooks/tests/help.ipynb
@@ -15,7 +15,7 @@
     {
      "data": {
       "text/markdown": [
-       "Enter a B expression or predicate to evaluate it.\n",
+       "Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use `:load` to load an external machine file.\n",
        "\n",
        "You can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n",
        "\n",
@@ -24,7 +24,7 @@
        "* `:eval` - Evaluate a formula and display the result.\n",
        "* `:solve` - Solve a predicate with the specified solver.\n",
        "* `:table` - Display an expression as a table.\n",
-       "* `:type` - Display the type of a formula.\n",
+       "* `:type` - Display the static type of a formula.\n",
        "* `:prettyprint` - Pretty-print a predicate.\n",
        "* `:let` - Evaluate an expression and store it in a local variable.\n",
        "* `:unlet` - Remove a local variable.\n",
@@ -32,13 +32,13 @@
        "\n",
        "## Animation\n",
        "\n",
-       "* `::load` - Load the machine source code given in the cell body.\n",
-       "* `:load` - Load the machine from the given path.\n",
+       "* `::load` - Load a B machine from the given source code.\n",
+       "* `:load` - Load a machine from a file.\n",
        "* `:constants` - Set up the current machine's constants.\n",
        "* `:init` - Initialise the current machine with the specified predicate\n",
        "* `:exec` - Execute an operation.\n",
        "* `:browse` - Show information about the current state.\n",
-       "* `:trace` - Display all states and transitions in the current trace.\n",
+       "* `:trace` - Display all states and executed operations in the current trace.\n",
        "* `:goto` - Go to the state with the specified index in the current trace.\n",
        "* `:find` - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
        "\n",
@@ -64,27 +64,27 @@
        "* `:version` - Display version info about the ProB CLI and ProB 2.\n"
       ],
       "text/plain": [
-       "Enter a B expression or predicate to evaluate it.\n",
+       "Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use :load to load an external machine file.\n",
        "You can also use any of the following commands. For more help on a particular command, run :help commandname.\n",
        "\n",
        "Evaluation:\n",
        ":eval - Evaluate a formula and display the result.\n",
        ":solve - Solve a predicate with the specified solver.\n",
        ":table - Display an expression as a table.\n",
-       ":type - Display the type of a formula.\n",
+       ":type - Display the static type of a formula.\n",
        ":prettyprint - Pretty-print a predicate.\n",
        ":let - Evaluate an expression and store it in a local variable.\n",
        ":unlet - Remove a local variable.\n",
        ":assert - Ensure that the predicate is true, and show an error otherwise.\n",
        "\n",
        "Animation:\n",
-       "::load - Load the machine source code given in the cell body.\n",
-       ":load - Load the machine from the given path.\n",
+       "::load - Load a B machine from the given source code.\n",
+       ":load - Load a machine from a file.\n",
        ":constants - Set up the current machine's constants.\n",
        ":init - Initialise the current machine with the specified predicate\n",
        ":exec - Execute an operation.\n",
        ":browse - Show information about the current state.\n",
-       ":trace - Display all states and transitions in the current trace.\n",
+       ":trace - Display all states and executed operations in the current trace.\n",
        ":goto - Go to the state with the specified index in the current trace.\n",
        ":find - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
        "\n",
@@ -156,19 +156,19 @@
        ":load FILENAME [PREF=VALUE ...]\n",
        "```\n",
        "\n",
-       "Load the machine from the given path.\n",
+       "Load a machine from a file.\n",
        "\n",
-       "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
+       "The file path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
        "\n",
-       "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
+       "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
       ],
       "text/plain": [
        ":load FILENAME [PREF=VALUE ...]\n",
-       "Load the machine from the given path.\n",
+       "Load a machine from a file.\n",
        "\n",
-       "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
+       "The file path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
        "\n",
-       "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
+       "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
       ]
      },
      "execution_count": 3,
@@ -189,28 +189,44 @@
      "data": {
       "text/markdown": [
        "```\n",
+       "MACHINE\n",
+       "...\n",
+       "END\n",
+       "\n",
+       "// or\n",
+       "\n",
        "::load [PREF=VALUE ...]\n",
        "MACHINE\n",
        "...\n",
        "END\n",
        "```\n",
        "\n",
-       "Load the machine source code given in the cell body.\n",
+       "Load a B machine from the given source code.\n",
+       "\n",
+       "Normally you do not need to explicitly call `::load` to load a machine from a cell. If you input the source code for a B machine without any command before it, it is loaded automatically.\n",
        "\n",
        "There must be a newline between the `::load` command name and the machine code.\n",
        "\n",
-       "Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
+       "If you use an explicit `::load` command, there must be a newline between `::load` and the machine source code. On the same line as `::load`, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
       ],
       "text/plain": [
+       "MACHINE\n",
+       "...\n",
+       "END\n",
+       "\n",
+       "// or\n",
+       "\n",
        "::load [PREF=VALUE ...]\n",
        "MACHINE\n",
        "...\n",
        "END\n",
-       "Load the machine source code given in the cell body.\n",
+       "Load a B machine from the given source code.\n",
+       "\n",
+       "Normally you do not need to explicitly call `::load` to load a machine from a cell. If you input the source code for a B machine without any command before it, it is loaded automatically.\n",
        "\n",
        "There must be a newline between the `::load` command name and the machine code.\n",
        "\n",
-       "Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
+       "If you use an explicit `::load` command, there must be a newline between `::load` and the machine source code. On the same line as `::load`, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
       ]
      },
      "execution_count": 4,
@@ -269,19 +285,19 @@
        ":load FILENAME [PREF=VALUE ...]\n",
        "```\n",
        "\n",
-       "Load the machine from the given path.\n",
+       "Load a machine from a file.\n",
        "\n",
-       "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
+       "The file path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
        "\n",
-       "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
+       "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
       ],
       "text/plain": [
        ":load FILENAME [PREF=VALUE ...]\n",
-       "Load the machine from the given path.\n",
+       "Load a machine from a file.\n",
        "\n",
-       "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
+       "The file path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
        "\n",
-       "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
+       "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
       ]
      },
      "execution_count": 6,
diff --git a/notebooks/tests/let.ipynb b/notebooks/tests/let.ipynb
index 0896dfd942c6cc5184283da00bdbbad69e7c5f91..630ec72c1808900863bcdeabb6aa7a669a118305 100644
--- a/notebooks/tests/let.ipynb
+++ b/notebooks/tests/let.ipynb
@@ -14,7 +14,9 @@
        "\n",
        "Evaluate an expression and store it in a local variable.\n",
        "\n",
-       "The expression is evaluated only once, in the current state, and its value is stored. Once set, variables are available in all states and are not affected by machine loads. A variable created by `:let` shadows any identifier from the machine with the same name.\n",
+       "The expression is evaluated once in the current state, and its value is stored. Once set, variables are available in all states. A variable created by `:let` shadows any identifier with the same name from the machine.\n",
+       "\n",
+       "Variables created by `:let` are retained even when a different machine is loaded. To remove a variable, use `:unlet`.\n",
        "\n",
        "**Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues."
       ],
@@ -22,7 +24,9 @@
        ":let NAME EXPR\n",
        "Evaluate an expression and store it in a local variable.\n",
        "\n",
-       "The expression is evaluated only once, in the current state, and its value is stored. Once set, variables are available in all states and are not affected by machine loads. A variable created by `:let` shadows any identifier from the machine with the same name.\n",
+       "The expression is evaluated once in the current state, and its value is stored. Once set, variables are available in all states. A variable created by `:let` shadows any identifier with the same name from the machine.\n",
+       "\n",
+       "Variables created by `:let` are retained even when a different machine is loaded. To remove a variable, use `:unlet`.\n",
        "\n",
        "**Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues."
       ]
diff --git a/notebooks/tests/load_cell.ipynb b/notebooks/tests/load_cell.ipynb
index f122de44ea4297c7a80be40f593a8517cedae978..7d3e416fa640214de0d82c67979e0d923739061c 100644
--- a/notebooks/tests/load_cell.ipynb
+++ b/notebooks/tests/load_cell.ipynb
@@ -9,28 +9,44 @@
      "data": {
       "text/markdown": [
        "```\n",
+       "MACHINE\n",
+       "...\n",
+       "END\n",
+       "\n",
+       "// or\n",
+       "\n",
        "::load [PREF=VALUE ...]\n",
        "MACHINE\n",
        "...\n",
        "END\n",
        "```\n",
        "\n",
-       "Load the machine source code given in the cell body.\n",
+       "Load a B machine from the given source code.\n",
+       "\n",
+       "Normally you do not need to explicitly call `::load` to load a machine from a cell. If you input the source code for a B machine without any command before it, it is loaded automatically.\n",
        "\n",
        "There must be a newline between the `::load` command name and the machine code.\n",
        "\n",
-       "Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
+       "If you use an explicit `::load` command, there must be a newline between `::load` and the machine source code. On the same line as `::load`, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
       ],
       "text/plain": [
+       "MACHINE\n",
+       "...\n",
+       "END\n",
+       "\n",
+       "// or\n",
+       "\n",
        "::load [PREF=VALUE ...]\n",
        "MACHINE\n",
        "...\n",
        "END\n",
-       "Load the machine source code given in the cell body.\n",
+       "Load a B machine from the given source code.\n",
+       "\n",
+       "Normally you do not need to explicitly call `::load` to load a machine from a cell. If you input the source code for a B machine without any command before it, it is loaded automatically.\n",
        "\n",
        "There must be a newline between the `::load` command name and the machine code.\n",
        "\n",
-       "Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
+       "If you use an explicit `::load` command, there must be a newline between `::load` and the machine source code. On the same line as `::load`, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
       ]
      },
      "execution_count": 1,
@@ -51,7 +67,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 1,
+   "execution_count": 2,
    "metadata": {},
    "outputs": [
     {
@@ -60,7 +76,7 @@
        "Loaded machine: dinge"
       ]
      },
-     "execution_count": 1,
+     "execution_count": 2,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -73,7 +89,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 2,
+   "execution_count": 3,
    "metadata": {},
    "outputs": [
     {
@@ -85,7 +101,7 @@
        "{EINS,ZWEI,DREI,VIER}"
       ]
      },
-     "execution_count": 2,
+     "execution_count": 3,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -103,7 +119,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 3,
+   "execution_count": 4,
    "metadata": {},
    "outputs": [
     {
@@ -112,7 +128,7 @@
        "Loaded machine: things"
       ]
      },
-     "execution_count": 3,
+     "execution_count": 4,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -126,7 +142,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 4,
+   "execution_count": 5,
    "metadata": {},
    "outputs": [
     {
@@ -138,7 +154,7 @@
        "{ONE,TWO,THREE,FOUR}"
       ]
      },
-     "execution_count": 4,
+     "execution_count": 5,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -156,7 +172,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 5,
+   "execution_count": 6,
    "metadata": {},
    "outputs": [
     {
@@ -165,7 +181,7 @@
        "Loaded machine: prefs"
       ]
      },
-     "execution_count": 5,
+     "execution_count": 6,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -178,7 +194,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 6,
+   "execution_count": 7,
    "metadata": {},
    "outputs": [
     {
@@ -190,7 +206,7 @@
        "{−5,−4,−3,−2,−1,0,1,2,3,4,5}"
       ]
      },
-     "execution_count": 6,
+     "execution_count": 7,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -208,7 +224,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 7,
+   "execution_count": 8,
    "metadata": {},
    "outputs": [
     {
@@ -229,21 +245,21 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 8,
+   "execution_count": 9,
    "metadata": {
     "scrolled": true
    },
    "outputs": [
     {
      "ename": "WithSourceCodeException",
-     "evalue": "de.prob.exception.ProBError: Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\nError: Identifier 'x' declared twice at (Line:Col[:File]) (Line:2 Col:17) and (Line:2 Col:14) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)",
+     "evalue": "de.prob.exception.ProBError: Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\nError: Identifier 'x' (local from duplicate) already declared at (Line:2 Col:14) (local from duplicate) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)",
      "output_type": "error",
      "traceback": [
       "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProlog said no.\u001b[0m",
       "\u001b[1m\u001b[30m2 errors:\u001b[0m",
       "\u001b[1m\u001b[31mError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
       "\u001b[1m\u001b[30m    CONSTANTS x, \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
-      "\u001b[1m\u001b[31mError: Identifier 'x' declared twice at (Line:Col[:File]) (Line:2 Col:17) and (Line:2 Col:14) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
+      "\u001b[1m\u001b[31mError: Identifier 'x' (local from duplicate) already declared at (Line:2 Col:14) (local from duplicate) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
       "\u001b[1m\u001b[30m    CONSTANTS x, \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m"
      ]
     }
@@ -258,7 +274,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 9,
+   "execution_count": 10,
    "metadata": {},
    "outputs": [
     {
diff --git a/notebooks/tests/load_file.ipynb b/notebooks/tests/load_file.ipynb
index 1fdbfea69bec2ba3a5b7d605291dba8283375b63..c57db3feb214068a41fb92b4ae55ca4def63402f 100644
--- a/notebooks/tests/load_file.ipynb
+++ b/notebooks/tests/load_file.ipynb
@@ -12,22 +12,19 @@
        ":load FILENAME [PREF=VALUE ...]\n",
        "```\n",
        "\n",
-       "Load the machine from the given path.\n",
+       "Load a machine from a file.\n",
        "\n",
-       "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
+       "The file path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
        "\n",
-       "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
+       "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
       ],
       "text/plain": [
-       "```\n",
        ":load FILENAME [PREF=VALUE ...]\n",
-       "```\n",
-       "\n",
-       "Load the machine from the given path.\n",
+       "Load a machine from a file.\n",
        "\n",
-       "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
+       "The file path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
        "\n",
-       "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
+       "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
       ]
      },
      "execution_count": 1,
diff --git a/notebooks/tests/pref.ipynb b/notebooks/tests/pref.ipynb
index 38d15556e48bcce4700a2f5bec5abb12f40c290e..8846808e49454b893c7db94bd82c4bbf131258dc 100644
--- a/notebooks/tests/pref.ipynb
+++ b/notebooks/tests/pref.ipynb
@@ -10,23 +10,25 @@
       "text/markdown": [
        "```\n",
        ":pref [NAME ...]\n",
+       "// or\n",
        ":pref NAME=VALUE [NAME=VALUE ...]\n",
        "```\n",
        "\n",
        "View or change the value of one or more preferences.\n",
        "\n",
-       "In the first form, the values of all given preferences are displayed (or all preferences, if none are given). In the second form, the given preference assignments are performed. The two forms cannot be mixed; it is not possible to view and change preferences in a single command.\n",
+       "In the first form, the values of the given preferences are displayed (or all preferences, if no preference names are given). In the second form, the values of the given preferences are changed. The two forms cannot be mixed; it is not possible to view and change preferences in a single command.\n",
        "\n",
-       "Certain preference changes do not take full effect when performed on a loaded machine. Such preferences must be assigned when the machine is loaded using the `::load` or `:load` command."
+       "Certain preference changes do not take full effect when performed on an already loaded machine. Such preferences must be set when the machine is loaded using the `::load` or `:load` command."
       ],
       "text/plain": [
        ":pref [NAME ...]\n",
+       "// or\n",
        ":pref NAME=VALUE [NAME=VALUE ...]\n",
        "View or change the value of one or more preferences.\n",
        "\n",
-       "In the first form, the values of all given preferences are displayed (or all preferences, if none are given). In the second form, the given preference assignments are performed. The two forms cannot be mixed; it is not possible to view and change preferences in a single command.\n",
+       "In the first form, the values of the given preferences are displayed (or all preferences, if no preference names are given). In the second form, the values of the given preferences are changed. The two forms cannot be mixed; it is not possible to view and change preferences in a single command.\n",
        "\n",
-       "Certain preference changes do not take full effect when performed on a loaded machine. Such preferences must be assigned when the machine is loaded using the `::load` or `:load` command."
+       "Certain preference changes do not take full effect when performed on an already loaded machine. Such preferences must be set when the machine is loaded using the `::load` or `:load` command."
       ]
      },
      "execution_count": 1,
@@ -57,14 +59,21 @@
        "ALLOW_INCOMPLETE_SETUP_CONSTANTS = false\n",
        "ALLOW_LOCAL_OPERATION_CALLS = false\n",
        "ALLOW_NEW_OPERATIONS_IN_REFINEMENT = false\n",
+       "ALLOW_OPERATION_CALLS_IN_EXPRESSIONS = false\n",
+       "ALLOW_OUTPUT_READING = false\n",
        "ALLOW_SIMULTANEOUS_ASSIGNMENTS = false\n",
        "ALLOW_UNTYPED_IDENTIFIERS = false\n",
+       "ALLOY_SCOPELESS_TRANSLATION = false\n",
+       "ALLOY_STRICT_INTEGERS = true\n",
+       "ALLOY_TRANSLATION_FOR_PROOF = false\n",
+       "ALLOY_USE_IMPLEMENTABLE_INTEGERS = false\n",
        "ATELIERB_KRT_PATH = krt\n",
        "BBRESULTS = false\n",
        "BOOL_AS_PREDICATE = false\n",
        "BUGLY = false\n",
        "CHR = false\n",
        "CLPFD = true\n",
+       "COMPILE_WHILE = true\n",
        "COMPRESSION = false\n",
        "CSE = false\n",
        "CSE_PRED = true\n",
@@ -73,25 +82,59 @@
        "CSP_STRIP_SOURCE_LOC = false\n",
        "DATA_VALIDATION = false\n",
        "DEFAULT_SETSIZE = 2\n",
-       "DETECT_LAMBDAS = false\n",
+       "DETECT_LAMBDAS = true\n",
        "DISPROVER_MODE = false\n",
        "DOT = /opt/local/bin/dot\n",
+       "DOT_ARC_COLORS = true\n",
        "DOT_ARGUMENTS = true\n",
        "DOT_COLOR_ARC = #006391\n",
        "DOT_COLOR_NODE = #99BF38\n",
        "DOT_COLOR_NODE_ERROR = #FF3800\n",
        "DOT_COLOR_NODE_GOAL = orange\n",
        "DOT_COLOR_NODE_OPEN = #F4E3C1\n",
+       "DOT_COLOUR_GOAL = true\n",
+       "DOT_CURRENT_NODE_SHAPE = doubleoctagon\n",
+       "DOT_DECOMPOSE_NODES = true\n",
+       "DOT_DEFINITIONS_SHOW_ALL = false\n",
+       "DOT_DEFINITIONS_USE_SUB_GRAPH = true\n",
+       "DOT_EDGE_FONT_SIZE = 12\n",
        "DOT_EDGE_LABELS = true\n",
        "DOT_ENGINE = dot\n",
+       "DOT_EVENT_HIERARCHY_EDGE_COL = #806040\n",
+       "DOT_EVENT_HIERARCHY_EXTENDS_COL = gray50\n",
+       "DOT_EVENT_HIERARCHY_GRD_KEEP_COL = #E0C080\n",
+       "DOT_EVENT_HIERARCHY_GRD_STRGTH_COL = gray83\n",
+       "DOT_EVENT_HIERARCHY_HORIZONTAL = true\n",
+       "DOT_EVENT_HIERARCHY_MCH_COL = gray95\n",
+       "DOT_EVENT_HIERARCHY_NEW_COL = #C06040\n",
+       "DOT_EVENT_HIERARCHY_REF_COL = #C0A060\n",
+       "DOT_EVENT_HIERARCHY_RENAME_COL = #E0E0A0\n",
+       "DOT_EVENT_HIERARCHY_RENAME_UNCHG_COL = #E0F0E0\n",
+       "DOT_EVENT_HIERARCHY_UNCHG_COL = gray92\n",
+       "DOT_EXPRESSION_NODE_SHAPE = record\n",
+       "DOT_FILL_NORMAL_NODES = false\n",
        "DOT_FUNCTIONS = false\n",
        "DOT_IDS = false\n",
        "DOT_INFO = true\n",
        "DOT_LOOPS = true\n",
+       "DOT_MACHINE_HIERARCHY_MAX_IDS = 0\n",
+       "DOT_NODE_FONT_SIZE = 12\n",
+       "DOT_NORMAL_NODE_SHAPE = box\n",
        "DOT_PEN_WIDTH = 2\n",
+       "DOT_PREDICATE_NODE_SHAPE = rect\n",
+       "DOT_PROJECTION_DEF_COL = solid\n",
+       "DOT_PROJECTION_DET_COL = black\n",
+       "DOT_PROJECTION_LABEL_LIMIT = 75\n",
+       "DOT_PROJECTION_NON_DEF_COL = dashed\n",
+       "DOT_PROJECTION_NON_DET_COL = #806040\n",
        "DOT_PROP = false\n",
        "DOT_ROOT = true\n",
+       "DOT_ROOT_SHAPE = invtriangle\n",
+       "DOT_SCOPE_LIMIT_COL = gray\n",
        "DOT_SHOW_OP_READ_WRITES = true\n",
+       "DOT_USE_CONSTANTS = true\n",
+       "DOT_USE_UNICODE = true\n",
+       "DOT_VARIABLE_MODIFICATION_HIDE_ONLY_WRITTEN = false\n",
        "DOUBLE_EVALUATION = true\n",
        "EDITOR = /usr/local/bin/bbedit\n",
        "EDITOR_GUI = /Applications/BBEdit.app\n",
@@ -104,6 +147,8 @@
        "INTERNAL_ARGUMENT_PREFIX = $none\n",
        "INVARIANT_CHECKING = true\n",
        "JAVA_PATH = /usr/bin/java\n",
+       "JVM_PARSER_ARGS = \n",
+       "JVM_PARSER_HEAP_MB = 0\n",
        "KODKOD = false\n",
        "KODKOD_MAX_NR_SOLS = 22\n",
        "KODKOD_ONLY_FULL = true\n",
@@ -112,12 +157,15 @@
        "KODKOD_SYMMETRY = 0\n",
        "LATEX_ENCODING = auto\n",
        "LATEX_GREEK_IDENTIFIERS = false\n",
+       "LIFT_EXISTS = false\n",
        "LTSMIN = ./lib/\n",
        "MAXINT = 3\n",
        "MAX_DISPLAY_SET = 100\n",
        "MAX_INITIALISATIONS = 4\n",
        "MAX_OPERATIONS = 10\n",
+       "MC_DC_Level = 2\n",
        "MEMO = false\n",
+       "MEMOIZE_FUNCTIONS = false\n",
        "MINIMAL_TEST_SUITES = true\n",
        "MININT = -1\n",
        "NDJSON_ERROR_LOG_FILE = \n",
@@ -128,6 +176,7 @@
        "PARTITION_PROPERTIES = true\n",
        "PARTITION_PROPERTIES_INLINE = true\n",
        "PERFORMANCE_INFO = false\n",
+       "PERFORMANCE_INFO_LIMIT = 100\n",
        "PGE = off\n",
        "PP_CS_STYLE_SEQUENCES = false\n",
        "PP_FROZEN_INFOS = false\n",
@@ -136,14 +185,19 @@
        "PROB2_TRACE_FILE_UNIQUE = false\n",
        "PROOF_INFO = true\n",
        "RAISE_ABORT_IMMEDIATELY = false\n",
+       "RANDOMISED_RESTART_INIT = false\n",
        "RANDOMISE_ENUMERATION_ORDER = false\n",
        "RANDOMISE_OPERATION_ORDER = false\n",
        "REMOVE_IMPLIED_CONSTRAINTS = false\n",
        "REPL_CACHE_PARSING = false\n",
        "REPL_UNICODE = false\n",
        "REQUIRE_OUTPUT_ASSIGNMENT = false\n",
+       "SAFETY_MODEL_CHECK = false\n",
+       "SAT_SUPPORTED_INTERPRETER = false\n",
        "SHOW_EVENTB_ANY_VALUES = false\n",
        "SMT = false\n",
+       "SMTLIB_BOOL_ARRAYS_TO_SETS = false\n",
+       "SMTLIB_PREPROCESS = false\n",
        "SMT_SUPPORTED_INTERPRETER = false\n",
        "SOLVER_STRENGTH = 0\n",
        "STATIC_ORDERING = false\n",
@@ -155,20 +209,24 @@
        "SYMBOLIC = false\n",
        "SYMBOLIC_MC_TRY_OTHER_SOLVERS = false\n",
        "SYMMETRY_MODE = off\n",
+       "SYNTAX_HIGHLIGHT = true\n",
        "TIME_OUT = 2500\n",
        "TK_CUSTOM_STATE_VIEW_FONT_NAME = \n",
        "TK_CUSTOM_STATE_VIEW_FONT_SIZE = 0\n",
        "TK_CUSTOM_STATE_VIEW_PADDING = 0\n",
        "TK_CUSTOM_STATE_VIEW_STRING_PADDING = 10\n",
+       "TK_CUSTOM_STATE_VIEW_VISIBLE = true\n",
        "TLC_WORKERS = 2\n",
        "TRACE_INFO = false\n",
        "TRACE_UPON_ERROR = false\n",
        "TRY_ATELIERB_PROVERS = false\n",
        "TRY_FIND_ABORT = false\n",
        "TYPE_CHECK_DEFINITIONS = false\n",
+       "USELESS_CODE_ELIMINATION = false\n",
+       "USE_IGNORE_PRAGMAS = false\n",
        "USE_RECORD_CONSTRUCTION = true\n",
+       "USE_SCOPE_DEFINITION = true\n",
        "WARN_IF_DEFINITION_HIDES_VARIABLE = true\n",
-       "WARN_WHEN_EXPANDING_INFINITE_CLOSURES = 5\n",
        "XML_ENCODING = auto\n"
       ]
      },
diff --git a/notebooks/tests/time.ipynb b/notebooks/tests/time.ipynb
index ff5eb7669bfc397acba9ff2a15bbb82a2d63f7af..016287b2fccfaa5b2e43b8b52957221ed9717b70 100644
--- a/notebooks/tests/time.ipynb
+++ b/notebooks/tests/time.ipynb
@@ -14,7 +14,7 @@
        "\n",
        "Execute the given command and measure how long it takes to execute.\n",
        "\n",
-       "The time is measured using Java's [`System.nanoTime()`](https://docs.oracle.com/javase/8/docs/api/java/lang/System.html#nanoTime--) method. The measured time is displayed with the full number of decimal places, but no guarantees are made about the actual resolution of the time measurement.\n",
+       "The time is internally measured using Java's [`System.nanoTime()`](https://docs.oracle.com/javase/8/docs/api/java/lang/System.html#nanoTime--) method. The measured time is displayed with nanosecond precision, but the actual resolution of the measurement is system-dependent and often much less accurate than nanoseconds.\n",
        "\n",
        "As with any measurement of execution time, there will likely be small differences between two measurements of the same command. The time is measured by the kernel rather than ProB, so it will include some overhead due to processing of the command by the kernel and communication with ProB."
       ],
@@ -22,7 +22,7 @@
        ":time COMMAND [ARGS ...]\n",
        "Execute the given command and measure how long it takes to execute.\n",
        "\n",
-       "The time is measured using Java's [`System.nanoTime()`](https://docs.oracle.com/javase/8/docs/api/java/lang/System.html#nanoTime--) method. The measured time is displayed with the full number of decimal places, but no guarantees are made about the actual resolution of the time measurement.\n",
+       "The time is internally measured using Java's [`System.nanoTime()`](https://docs.oracle.com/javase/8/docs/api/java/lang/System.html#nanoTime--) method. The measured time is displayed with nanosecond precision, but the actual resolution of the measurement is system-dependent and often much less accurate than nanoseconds.\n",
        "\n",
        "As with any measurement of execution time, there will likely be small differences between two measurements of the same command. The time is measured by the kernel rather than ProB, so it will include some overhead due to processing of the command by the kernel and communication with ProB."
       ]
@@ -51,10 +51,10 @@
     {
      "data": {
       "text/markdown": [
-       "Execution time: 1.029510290 seconds"
+       "Execution time: 1.034897011 seconds"
       ],
       "text/plain": [
-       "Execution time: 1.029510290 seconds"
+       "Execution time: 1.034897011 seconds"
       ]
      },
      "metadata": {},
@@ -90,10 +90,10 @@
     {
      "data": {
       "text/markdown": [
-       "Execution time: 1.156164498 seconds"
+       "Execution time: 1.206485155 seconds"
       ],
       "text/plain": [
-       "Execution time: 1.156164498 seconds"
+       "Execution time: 1.206485155 seconds"
       ]
      },
      "metadata": {},
diff --git a/notebooks/tests/trace.ipynb b/notebooks/tests/trace.ipynb
index 152964417a4450171ae66b85eab641640e85cb33..b395563c150b63aaf67d866cf563b676af4a4117 100644
--- a/notebooks/tests/trace.ipynb
+++ b/notebooks/tests/trace.ipynb
@@ -12,19 +12,19 @@
        ":trace\n",
        "```\n",
        "\n",
-       "Display all states and transitions in the current trace.\n",
+       "Display all states and executed operations in the current trace.\n",
        "\n",
        "Each state has an index, which can be passed to the `:goto` command to go to that state.\n",
        "\n",
-       "The first state (index -1) is always the root state. All other states are reached from the root state by following (previously executed) transitions."
+       "The first state (index -1) is always the root state. All other states are reached from the root state by following previously executed operations."
       ],
       "text/plain": [
        ":trace\n",
-       "Display all states and transitions in the current trace.\n",
+       "Display all states and executed operations in the current trace.\n",
        "\n",
        "Each state has an index, which can be passed to the `:goto` command to go to that state.\n",
        "\n",
-       "The first state (index -1) is always the root state. All other states are reached from the root state by following (previously executed) transitions."
+       "The first state (index -1) is always the root state. All other states are reached from the root state by following previously executed operations."
       ]
      },
      "execution_count": 1,
@@ -52,7 +52,7 @@
        "\n",
        "Use the `:trace` command to view the current trace and the indices of its states. Index -1 refers to the root state and is always available.\n",
        "\n",
-       "Going backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in a state *will* discard any parts of the trace after that state (and replace them with the destination state of the executed transition)."
+       "Going backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in an older state *will* discard any parts of the trace after that state, and replace them with the new state reached after executing the operation."
       ],
       "text/plain": [
        ":goto INDEX\n",
@@ -60,7 +60,7 @@
        "\n",
        "Use the `:trace` command to view the current trace and the indices of its states. Index -1 refers to the root state and is always available.\n",
        "\n",
-       "Going backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in a state *will* discard any parts of the trace after that state (and replace them with the destination state of the executed transition)."
+       "Going backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in an older state *will* discard any parts of the trace after that state, and replace them with the new state reached after executing the operation."
       ]
      },
      "execution_count": 2,
@@ -124,11 +124,11 @@
      "data": {
       "text/markdown": [
        "* -1: Root state\n",
-       "* 0: `$initialise_machine` **(current)**"
+       "* 0: `INITIALISATION()` **(current)**"
       ],
       "text/plain": [
        "-1: Root state\n",
-       "0: $initialise_machine (current)"
+       "0: INITIALISATION() (current)"
       ]
      },
      "execution_count": 5,
@@ -169,11 +169,11 @@
      "data": {
       "text/markdown": [
        "* -1: Root state **(current)**\n",
-       "* 0: `$initialise_machine`"
+       "* 0: `INITIALISATION()`"
       ],
       "text/plain": [
        "-1: Root state (current)\n",
-       "0: $initialise_machine"
+       "0: INITIALISATION()"
       ]
      },
      "execution_count": 7,
diff --git a/notebooks/tests/type.ipynb b/notebooks/tests/type.ipynb
index 7da998746306caa69f30e73063914c374687cd28..9745c402783131595a242f40667a38da9330145f 100644
--- a/notebooks/tests/type.ipynb
+++ b/notebooks/tests/type.ipynb
@@ -12,11 +12,15 @@
        ":type FORMULA\n",
        "```\n",
        "\n",
-       "Display the type of a formula."
+       "Display the static type of a formula.\n",
+       "\n",
+       "The type is displayed in B syntax. If the formula is a predicate, the type is `predicate`."
       ],
       "text/plain": [
        ":type FORMULA\n",
-       "Display the type of a formula."
+       "Display the static type of a formula.\n",
+       "\n",
+       "The type is displayed in B syntax. If the formula is a predicate, the type is `predicate`."
       ]
      },
      "execution_count": 1,
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index f4fe97ded7beb7c7fe1a21892db7994e7135638e..126842323fe8f8cd3bb965e14b4a998b60d8b72a 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -46,8 +46,9 @@ public final class AssertCommand implements Command {
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "This command is intended for verifying that a predicate is always true at a certain point in a notebook. Unlike normal evaluation (`:eval`), this command treats a $\\mathit{FALSE}$ result as an error. If the result is $\\mathit{TRUE}$, solutions for free variables (if any) are not displayed.\n\n"
-			+ "Only predicates and $\\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error.";
+		return "Unlike normal evaluation (`:eval`), this command treats a $\\mathit{FALSE}$ result as an error. If the result is $\\mathit{TRUE}$, solutions for free variables (if any) are not displayed.\n\n"
+			+ "Only predicates and $\\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error.\n\n"
+			+ "This command is intended for verifying that a condition holds at a certain point in the notebook. It may also be used in combination with the Jupyter Notebook [nbgrader](https://nbgrader.readthedocs.io/) extension for automatic checking/grading of exercises.";
 	}
 	
 	@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
index f65282fadabf0029779a94268507b599135bc8ba..852ea6f30b8cabc043f1525f8a42f01e8707aa85 100644
--- a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
@@ -49,7 +49,7 @@ public final class BrowseCommand implements Command {
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of transitions that are available in the current state.";
+		return "The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of enabled operations (and possible parameter values) in the current state.";
 	}
 	
 	private static @NotNull String listToString(final List<String> list) {
diff --git a/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java b/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java
index bd961b22a355a2bf7d7e209313a28a0658241f69..d51a4f4c968c5df5fcdf2e112c3afdab59bdf01d 100644
--- a/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java
@@ -31,7 +31,7 @@ public final class BsymbCommand implements Command {
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "";
+		return "If you want to use bsymb.sty commands in your Markdown cells, you *must* run `:bsymb` first. Otherwise the commands may not be reliably available after reopening the notebook.";
 	}
 	
 	@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
index 3e639832e26089837f10611fc63139567c18a7c7..38267a9f3c7b81a8f5c6340d84a2eb5430a4070b 100644
--- a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
@@ -32,7 +32,7 @@ public final class EvalCommand implements Command {
 	
 	@Override
 	public @NotNull String getSyntax() {
-		return ":eval FORMULA";
+		return "FORMULA\n// or\n:eval FORMULA";
 	}
 	
 	@Override
@@ -42,8 +42,8 @@ public final class EvalCommand implements Command {
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "This is equivalent to inputting the formula without a command name.\n\n"
-			+ "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed.";
+		return "Normally you do not need to explicitly call `:eval` to evaluate formulas. If you input a formula without any command before it, it is evaluated automatically (e. g. `:eval 1 + 2` is equivalent to just `1 + 2`).\n\n"
+			+ "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed. For more control about which solver is used to solve the predicate, use the `:solve` command.";
 	}
 	
 	@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
index e41a07e7f03fe4207c14c050a77218808c6a751b..43e607d1658ffabc7ca977d1ddf2db10e4c143a3 100644
--- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
@@ -48,7 +48,8 @@ public final class ExecCommand implements Command {
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "A transition for the given operation is found and executed. If the optional predicate is specified, a transition is found for which the predicate is $\\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have.";
+		return "The predicate is used to select the operation's parameter values. The parameters can be fully specified explicitly (e. g. `:exec op param1 = 123 & param2 = {1, 2}`), or they can be partially constrained (e. g. `:exec op param1 > 100 & card(param2) >= 2`) to let ProB find a valid combination of parameters. If there are multiple valid combinations of parameters that satisfy the predicate, it is undefined which one is selected by ProB.\n\n"
+			+ "If no predicate is specified, the parameters are not constrained, and ProB will select an arbitrary valid combination of parameters.";
 	}
 	
 	@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/FindCommand.java b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
index d9ee3c6c43016c63fa0c3894705a7d4bfb47c652..ebf07385be3a57aef6e1a613376145bde213c9d9 100644
--- a/src/main/java/de/prob2/jupyter/commands/FindCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
@@ -44,7 +44,8 @@ public final class FindCommand implements Command {
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "If such a state is found, it is made the current state, otherwise an error is displayed.\n\nNote that this command does not necessarily find a valid *trace* to the found state. Instead, in some cases a single \"fake\" transition is added to the trace, which goes directly to the found state and does not use the machine's operations to reach it.";
+		return "If such a state is found, it is made the current state, otherwise an error is displayed.\n\n"
+			+ "Note that this command does not necessarily find a valid *trace* to the found state. Instead, this command may a single \"fake\" transition to the trace, which goes directly to the found state and does not use the machine's operations to reach it. Such a state may or may not be reachable by a sequence of normal operations.";
 	}
 	
 	@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/GotoCommand.java b/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
index 497202edfaf978ecad1dd65cc09b9a2186e6faec..e02ec183bd36fe705eee25434b30a42e5aac4b6c 100644
--- a/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
@@ -40,7 +40,8 @@ public final class GotoCommand implements Command {
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "Use the `:trace` command to view the current trace and the indices of its states. Index -1 refers to the root state and is always available.\n\nGoing backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in a state *will* discard any parts of the trace after that state (and replace them with the destination state of the executed transition).";
+		return "Use the `:trace` command to view the current trace and the indices of its states. Index -1 refers to the root state and is always available.\n\n"
+			+ "Going backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in an older state *will* discard any parts of the trace after that state, and replace them with the new state reached after executing the operation.";
 	}
 	
 	@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
index c8a510a3266a98af6c97c5477e56f04869830217..1ce3f6e60c0eaf02a7f9efbbd873847946fd1d0d 100644
--- a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
@@ -91,8 +91,8 @@ public final class HelpCommand implements Command {
 		final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
 		final List<String> args = CommandUtils.splitArgs(argString);
 		if (args.isEmpty()) {
-			final StringBuilder sb = new StringBuilder("Enter a B expression or predicate to evaluate it.\nYou can also use any of the following commands. For more help on a particular command, run :help commandname.\n");
-			final StringBuilder sbMarkdown = new StringBuilder("Enter a B expression or predicate to evaluate it.\n\nYou can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n");
+			final StringBuilder sb = new StringBuilder("Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use :load to load an external machine file.\nYou can also use any of the following commands. For more help on a particular command, run :help commandname.\n");
+			final StringBuilder sbMarkdown = new StringBuilder("Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use `:load` to load an external machine file.\n\nYou can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n");
 			
 			final Map<Class<? extends Command>, Command> commandsByClass = kernel.getCommands()
 				.values()
diff --git a/src/main/java/de/prob2/jupyter/commands/LetCommand.java b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
index 35669d31443b76b3123aca9b31cd42c9644e886e..a8d5eb078f1ae889c8e520e24af4d2721d95475e 100644
--- a/src/main/java/de/prob2/jupyter/commands/LetCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
@@ -47,7 +47,9 @@ public final class LetCommand implements Command {
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "The expression is evaluated only once, in the current state, and its value is stored. Once set, variables are available in all states and are not affected by machine loads. A variable created by `:let` shadows any identifier from the machine with the same name.\n\n**Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues.";
+		return "The expression is evaluated once in the current state, and its value is stored. Once set, variables are available in all states. A variable created by `:let` shadows any identifier with the same name from the machine.\n\n"
+			+ "Variables created by `:let` are retained even when a different machine is loaded. To remove a variable, use `:unlet`.\n\n"
+			+ "**Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues.";
 	}
 	
 	@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
index 08ee240eae2763504aedede5233ed37fb6c92d69..0056fbcf0276d5b54ddc77b4c4b7d5553afa38bb 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
@@ -44,18 +44,19 @@ public final class LoadCellCommand implements Command {
 	
 	@Override
 	public @NotNull String getSyntax() {
-		return "::load [PREF=VALUE ...]\nMACHINE\n...\nEND";
+		return "MACHINE\n...\nEND\n\n// or\n\n::load [PREF=VALUE ...]\nMACHINE\n...\nEND";
 	}
 	
 	@Override
 	public @NotNull String getShortHelp() {
-		return "Load the machine source code given in the cell body.";
+		return "Load a B machine from the given source code.";
 	}
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "There must be a newline between the `::load` command name and the machine code.\n\n"
-			+ "Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded.";
+		return "Normally you do not need to explicitly call `::load` to load a machine from a cell. If you input the source code for a B machine without any command before it, it is loaded automatically.\n\n"
+			+ "There must be a newline between the `::load` command name and the machine code.\n\n"
+			+ "If you use an explicit `::load` command, there must be a newline between `::load` and the machine source code. On the same line as `::load`, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded.";
 	}
 	
 	@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
index 04fb3859d9c48d1fc8f286b755e376b7020c4aab..1b4f2c47b02a62b182867c8c99f496b69f0e42f6 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
@@ -61,13 +61,13 @@ public final class LoadFileCommand implements Command {
 	
 	@Override
 	public @NotNull String getShortHelp() {
-		return "Load the machine from the given path.";
+		return "Load a machine from a file.";
 	}
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n\n"
-			+ "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded.";
+		return "The file path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n\n"
+			+ "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded.";
 	}
 	
 	@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
index 28df02a872c6a3a0671853b8df8dccd1846698fb..3672b8ba1298a72e2754842c19dae717c054e4af 100644
--- a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
@@ -37,7 +37,7 @@ public final class PrefCommand implements Command {
 	
 	@Override
 	public @NotNull String getSyntax() {
-		return ":pref [NAME ...]\n:pref NAME=VALUE [NAME=VALUE ...]";
+		return ":pref [NAME ...]\n// or\n:pref NAME=VALUE [NAME=VALUE ...]";
 	}
 	
 	@Override
@@ -47,8 +47,8 @@ public final class PrefCommand implements Command {
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "In the first form, the values of all given preferences are displayed (or all preferences, if none are given). In the second form, the given preference assignments are performed. The two forms cannot be mixed; it is not possible to view and change preferences in a single command.\n\n"
-			+ "Certain preference changes do not take full effect when performed on a loaded machine. Such preferences must be assigned when the machine is loaded using the `::load` or `:load` command.";
+		return "In the first form, the values of the given preferences are displayed (or all preferences, if no preference names are given). In the second form, the values of the given preferences are changed. The two forms cannot be mixed; it is not possible to view and change preferences in a single command.\n\n"
+			+ "Certain preference changes do not take full effect when performed on an already loaded machine. Such preferences must be set when the machine is loaded using the `::load` or `:load` command.";
 	}
 	
 	@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java b/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
index c9270d891b10aeb46d6693887d9514272fdec983..ee46d95d99a467271383c08ac4329363bd6adfdc 100644
--- a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
@@ -42,7 +42,7 @@ public final class TimeCommand implements Command {
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "The time is internally measured using Java's [`System.nanoTime()`](https://docs.oracle.com/javase/8/docs/api/java/lang/System.html#nanoTime--) method. The measured time is displayed with nanosecond precision, but the actual resolution of the measurement is system-dependent and often much larger than nanoseconds.\n\n"
+		return "The time is internally measured using Java's [`System.nanoTime()`](https://docs.oracle.com/javase/8/docs/api/java/lang/System.html#nanoTime--) method. The measured time is displayed with nanosecond precision, but the actual resolution of the measurement is system-dependent and often much less accurate than nanoseconds.\n\n"
 			+ "As with any measurement of execution time, there will likely be small differences between two measurements of the same command. The time is measured by the kernel rather than ProB, so it will include some overhead due to processing of the command by the kernel and communication with ProB.";
 	}
 	
diff --git a/src/main/java/de/prob2/jupyter/commands/TraceCommand.java b/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
index 773f1bc9676fc802cf4f238d9ddd7a57be6a720a..c3f97bc3fb0bbed2fa7efd955d87e2fc6ebedae5 100644
--- a/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
@@ -38,12 +38,13 @@ public final class TraceCommand implements Command {
 	
 	@Override
 	public @NotNull String getShortHelp() {
-		return "Display all states and transitions in the current trace.";
+		return "Display all states and executed operations in the current trace.";
 	}
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "Each state has an index, which can be passed to the `:goto` command to go to that state.\n\nThe first state (index -1) is always the root state. All other states are reached from the root state by following (previously executed) transitions.";
+		return "Each state has an index, which can be passed to the `:goto` command to go to that state.\n\n"
+			+ "The first state (index -1) is always the root state. All other states are reached from the root state by following previously executed operations.";
 	}
 	
 	@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
index 8c0de732081f206952e380c7b483ad8237316e76..f1030356b7174b7d6a81b3e5a0c89b9022852dd2 100644
--- a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
@@ -41,12 +41,12 @@ public final class TypeCommand implements Command {
 	
 	@Override
 	public @NotNull String getShortHelp() {
-		return "Display the type of a formula.";
+		return "Display the static type of a formula.";
 	}
 	
 	@Override
 	public @NotNull String getHelpBody() {
-		return "";
+		return "The type is displayed in B syntax. If the formula is a predicate, the type is `predicate`.";
 	}
 	
 	@Override