diff --git a/notebooks/manual/FloatsReals.ipynb b/notebooks/manual/FloatsReals.ipynb index 41dc6e1ca0ae19eff686317d2af8f2dcdd9338a5..90e15ffb733bd26a3af0c6b9ed4181e19f165966 100644 --- a/notebooks/manual/FloatsReals.ipynb +++ b/notebooks/manual/FloatsReals.ipynb @@ -786,7 +786,24 @@ "cell_type": "markdown", "id": "cc7e1768", "metadata": {}, - "source": [] + "source": [ + "## Event-B Theories\n", + "Event-B does not have support for reals or floats as basic type but one can use the theory plugin.\n", + "\n", + "[https://prob.hhu.de/w/index.php?title=Event-B_Theories]\n", + "\n", + "To be able to view reals in ProB within Rodin you need to install a recent nightly build: [https://www3.hhu.de/stups/rodin/prob1/nightly]\n", + "\n", + "You need to use one of the standard theories.\n", + "\n", + "To write your own theory you should add an axiomatic type called REAL, FLOAT or the unicode R for reals.\n", + "Then you have to define axiomatic operators and link them to ProB's real operators.\n", + "You can do this either\n", + "* using a theory mapping file (.ptm extension) which needs to be put into the Rodin project, see [https://prob.hhu.de/w/index.php?title=Event-B_Theories]\n", + "* or use the same name as the external functions above (e.g., RSQRT); in this way ProB will do the mapping automatically.\n", + "\n", + "\n" + ] } ], "metadata": {