diff --git a/notebooks/tests/help.ipynb b/notebooks/tests/help.ipynb
index d941068d066705085b817b25590a264234e6744e..58842a6b85bb1d17057ba8e853b59db2e7ba5852 100644
--- a/notebooks/tests/help.ipynb
+++ b/notebooks/tests/help.ipynb
@@ -15,61 +15,72 @@
     {
      "data": {
       "text/markdown": [
-       "Type a valid B expression, or one of the following commands:\n",
+       "Enter a B expression or predicate to evaluate it.\n",
        "\n",
-       "* `::load` Load the machine source code given in the cell body.\n",
-       "* `::render` Render some content with the specified MIME type.\n",
-       "* `:assert` Ensure that the predicate is true, and show an error otherwise.\n",
-       "* `:browse` Show information about the current state.\n",
-       "* `:check` Check the machine's properties, invariant, or assertions in the current state.\n",
-       "* `:constants` Set up the current machine's constants.\n",
-       "* `:dot` Execute and show a dot visualisation.\n",
-       "* `:eval` Evaluate a formula and display the result.\n",
-       "* `:exec` Execute an operation.\n",
-       "* `:find` Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
-       "* `:goto` Go to the state with the specified index in the current trace.\n",
-       "* `:groovy` Evaluate the given Groovy expression.\n",
-       "* `:help` Display help for a specific command, or general help about the REPL.\n",
-       "* `:init` Initialise the current machine with the specified predicate\n",
-       "* `:load` Load the machine from the given path.\n",
-       "* `:pref` View or change the value of one or more preferences.\n",
-       "* `:prettyprint` Pretty-print a predicate.\n",
-       "* `:show` Show the machine's animation function visualisation for the current state.\n",
-       "* `:solve` Solve a predicate with the specified solver.\n",
-       "* `:stats` Show statistics about the state space.\n",
-       "* `:table` Display an expression as a table.\n",
-       "* `:time` Execute the given command and measure how long it takes to execute.\n",
-       "* `:trace` Display all states and transitions in the current trace.\n",
-       "* `:type` Display the type of a formula.\n",
-       "* `:version` Display version info about the ProB CLI and ProB 2.\n"
+       "You can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n",
+       "\n",
+       "* `::load` - Load the machine source code given in the cell body.\n",
+       "* `::render` - Render some content with the specified MIME type.\n",
+       "* `:assert` - Ensure that the predicate is true, and show an error otherwise.\n",
+       "* `:browse` - Show information about the current state.\n",
+       "* `:bsymb` - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\n",
+       "* `:check` - Check the machine's properties, invariant, or assertions in the current state.\n",
+       "* `:constants` - Set up the current machine's constants.\n",
+       "* `:dot` - Execute and show a dot visualisation.\n",
+       "* `:eval` - Evaluate a formula and display the result.\n",
+       "* `:exec` - Execute an operation.\n",
+       "* `:find` - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
+       "* `:goto` - Go to the state with the specified index in the current trace.\n",
+       "* `:groovy` - Evaluate the given Groovy expression.\n",
+       "* `:help` - Display help for a specific command, or general help about the REPL.\n",
+       "* `:init` - Initialise the current machine with the specified predicate\n",
+       "* `:let` - Evaluate an expression and store it in a local variable.\n",
+       "* `:load` - Load the machine from the given path.\n",
+       "* `:modelcheck` - Run the ProB model checker on the current model.\n",
+       "* `:pref` - View or change the value of one or more preferences.\n",
+       "* `:prettyprint` - Pretty-print a predicate.\n",
+       "* `:show` - Show the machine's animation function visualisation for the current state.\n",
+       "* `:solve` - Solve a predicate with the specified solver.\n",
+       "* `:stats` - Show statistics about the state space.\n",
+       "* `:table` - Display an expression as a table.\n",
+       "* `:time` - Execute the given command and measure how long it takes to execute.\n",
+       "* `:trace` - Display all states and transitions in the current trace.\n",
+       "* `:type` - Display the type of a formula.\n",
+       "* `:unlet` - Remove a local variable.\n",
+       "* `:version` - Display version info about the ProB CLI and ProB 2.\n"
       ],
       "text/plain": [
-       "Type a valid B expression, or one of the following commands:\n",
-       "::load Load the machine source code given in the cell body.\n",
-       "::render Render some content with the specified MIME type.\n",
-       ":assert Ensure that the predicate is true, and show an error otherwise.\n",
-       ":browse Show information about the current state.\n",
-       ":check Check the machine's properties, invariant, or assertions in the current state.\n",
-       ":constants Set up the current machine's constants.\n",
-       ":dot Execute and show a dot visualisation.\n",
-       ":eval Evaluate a formula and display the result.\n",
-       ":exec Execute an operation.\n",
-       ":find Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
-       ":goto Go to the state with the specified index in the current trace.\n",
-       ":groovy Evaluate the given Groovy expression.\n",
-       ":help Display help for a specific command, or general help about the REPL.\n",
-       ":init Initialise the current machine with the specified predicate\n",
-       ":load Load the machine from the given path.\n",
-       ":pref View or change the value of one or more preferences.\n",
-       ":prettyprint Pretty-print a predicate.\n",
-       ":show Show the machine's animation function visualisation for the current state.\n",
-       ":solve Solve a predicate with the specified solver.\n",
-       ":stats Show statistics about the state space.\n",
-       ":table Display an expression as a table.\n",
-       ":time Execute the given command and measure how long it takes to execute.\n",
-       ":trace Display all states and transitions in the current trace.\n",
-       ":type Display the type of a formula.\n",
-       ":version Display version info about the ProB CLI and ProB 2.\n"
+       "Enter a B expression or predicate to evaluate it.\n",
+       "You can also use any of the following commands. For more help on a particular command, run :help commandname.\n",
+       "::load - Load the machine source code given in the cell body.\n",
+       "::render - Render some content with the specified MIME type.\n",
+       ":assert - Ensure that the predicate is true, and show an error otherwise.\n",
+       ":browse - Show information about the current state.\n",
+       ":bsymb - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\n",
+       ":check - Check the machine's properties, invariant, or assertions in the current state.\n",
+       ":constants - Set up the current machine's constants.\n",
+       ":dot - Execute and show a dot visualisation.\n",
+       ":eval - Evaluate a formula and display the result.\n",
+       ":exec - Execute an operation.\n",
+       ":find - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
+       ":goto - Go to the state with the specified index in the current trace.\n",
+       ":groovy - Evaluate the given Groovy expression.\n",
+       ":help - Display help for a specific command, or general help about the REPL.\n",
+       ":init - Initialise the current machine with the specified predicate\n",
+       ":let - Evaluate an expression and store it in a local variable.\n",
+       ":load - Load the machine from the given path.\n",
+       ":modelcheck - Run the ProB model checker on the current model.\n",
+       ":pref - View or change the value of one or more preferences.\n",
+       ":prettyprint - Pretty-print a predicate.\n",
+       ":show - Show the machine's animation function visualisation for the current state.\n",
+       ":solve - Solve a predicate with the specified solver.\n",
+       ":stats - Show statistics about the state space.\n",
+       ":table - Display an expression as a table.\n",
+       ":time - Execute the given command and measure how long it takes to execute.\n",
+       ":trace - Display all states and transitions in the current trace.\n",
+       ":type - Display the type of a formula.\n",
+       ":unlet - Remove a local variable.\n",
+       ":version - Display version info about the ProB CLI and ProB 2.\n"
       ]
      },
      "execution_count": 1,
diff --git a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
index 9355b91d24f976c80493610413ebf0406685dd42..31badb3aa333b95dd04f721660f24b6da3b9ac91 100644
--- a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
@@ -46,8 +46,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("Type a valid B expression, or one of the following commands:\n");
-			final StringBuilder sbMarkdown = new StringBuilder("Type a valid B expression, or one of the following commands:\n\n");
+			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\n");
 			new TreeMap<>(kernel.getCommands()).forEach((commandName, command) -> {
 				sb.append(commandName);
 				sb.append(" - ");