diff --git a/notebooks/manual/FloatsReals.ipynb b/notebooks/manual/FloatsReals.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..c584d197eb90c8ff9b29d4c2983ff921df34fefd
--- /dev/null
+++ b/notebooks/manual/FloatsReals.ipynb
@@ -0,0 +1,484 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "85001897",
+ "metadata": {},
+ "source": [
+ "# Reals and Floats in ProB\n",
+ "\n",
+ "### Michael Leuschel\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "42473a5e",
+ "metadata": {},
+ "source": [
+ "## Classical B\n",
+ "\n",
+ "In Atelier-B the following two types were added to the B language:\n",
+ "* REAL\n",
+ "* FLOAT\n",
+ "\n",
+ "ProB treats these keywords as synonyms for a new base type.\n",
+ "The current representation in ProB are floating point numbers; but this\n",
+ "will probably change in the future, at least for the REAL type.\n",
+ "\n",
+ "One can now also use literals in decimal point notation for REAL and FLOAT."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "id": "cf76baf3",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1.0$"
+ ],
+ "text/plain": [
+ "1.0"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1.0"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "id": "941433ba",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1.0 : REAL & 1.0 : FLOAT"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "f7398e0e",
+ "metadata": {},
+ "source": [
+ "### Arithmetic Operators\n",
+ "\n",
+ "The documentation of Atelier-B is not entirely consistent according to which\n",
+ "operators to use.\n",
+ "In ProB you can use the standard arithmetic operators also for\n",
+ "floats:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "65a66ec9",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$2.0$"
+ ],
+ "text/plain": [
+ "2.0"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1.0 + 1.0"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "id": "35ce95d5",
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "2.0 * 2.0 < 2.1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "id": "531aa72d",
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "2.0 * 2.0 < 2.0 + 2.0"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "9066aa50",
+ "metadata": {},
+ "source": [
+ "You can control whether to allow arithmetic operators for reals\n",
+ "in ProB via the preference ```ALLOW_REALS```.\n",
+ "By default reals are allowed for classical B and disallowed for Event-B.\n",
+ "The only disadvantage of allowing reals is that the arithmetic operators\n",
+ "are overloaded, which may require stronger typing.\n",
+ "E.g., without ```x:INT``` you get an error that the type of x and y cannot be inferred, when reals are allowed:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "id": "528e647d",
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = -1$\n",
+ "* $\\mathit{y} = 0$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = −1\n",
+ "\ty = 0"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x:INT & x < y"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "02b86510",
+ "metadata": {},
+ "source": [
+ "### Constraint solving\n",
+ "\n",
+ "Constraint solving and enumeration is very limited in ProB.\n",
+ "This will change in future.\n",
+ "Currently ProB will enumerate a few random values for unspecified reals,\n",
+ "and then stop with an enumeration warning."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "id": "9356ea2c",
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = 0.0$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 0.0"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x:REAL"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "id": "b6d8671d",
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = 1.0$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 1.0"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x + 1.0 = 2.0"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "13388af0",
+ "metadata": {},
+ "source": [
+ "### Other Operators\n",
+ "\n",
+ "The standard library ```LibraryReals.def``` provides many functions\n",
+ "over reals as external functions.\n",
+ "These functions typically start with a capital R.\n",
+ "The functions are available in the REPL (aka console) but\n",
+ "one needs to import ```LibraryReals.def``` to use them in a B machine.\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "id": "df6d2cd0",
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1.4142135623730951$"
+ ],
+ "text/plain": [
+ "1.4142135623730951"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "RSQRT(2.0)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "id": "d2daab50",
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1.2246467991473532E-16$"
+ ],
+ "text/plain": [
+ "1.2246467991473532E-16"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "RSIN(RPI)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "id": "481e4f68",
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{r} = 1.0$\n",
+ "* $\\mathit{x} = 0.5$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tr = 1.0\n",
+ "\tx = 0.5"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "r=RPOW(RSIN(x),2.0)+RPOW(RCOS(x),2.0) & x=0.5"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "id": "bfd74a24",
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{r} = 1.0$\n",
+ "* $\\mathit{x} = 10.5$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tr = 1.0\n",
+ "\tx = 10.5"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "r=RPOW(RSIN(x),2.0)+RPOW(RCOS(x),2.0) & x=10.5"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "34ca2773",
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}