diff --git a/notebooks/models/scheduler.ipynb b/notebooks/models/scheduler.ipynb
index ef4123c92c0a4e038368887fbee61c3ca71a5152..ad0c22204ce2516ad9a5435b6f46743b6cd29b84 100644
--- a/notebooks/models/scheduler.ipynb
+++ b/notebooks/models/scheduler.ipynb
@@ -76,11 +76,11 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: NOT-INITIALISED",
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: NOT-INITIALISED",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: NOT-INITIALISED\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mNOT-INITIALISED\u001b[0m"
]
}
],
@@ -248,7 +248,7 @@
{
"data": {
"text/markdown": [
- "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ "$\\def\\emptyset{\\mathord\\varnothing}\\emptyset$"
],
"text/plain": [
"∅"
diff --git a/notebooks/tutorials/Functional_Programming_in_B.ipynb b/notebooks/tutorials/Functional_Programming_in_B.ipynb
index b86c9b0521d486568af4a0532db4ffb12f08aa81..806c984d891b86c2d6fa989fccd68a876b58c145 100644
--- a/notebooks/tutorials/Functional_Programming_in_B.ipynb
+++ b/notebooks/tutorials/Functional_Programming_in_B.ipynb
@@ -23,11 +23,11 @@
{
"data": {
"text/markdown": [
- "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\mathit{TRUE}$\n",
+ "$\\def\\qdot{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\def\\intg{\\mathord{\\mathbb Z}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{r2} = \\{1,4,9,16,25,36,49,64,81,100\\}$\n",
- "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\lambda\\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid\\mathit{x} * \\mathit{x})$\n",
+ "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\lambda\\mathit{x}\\qdot(\\mathit{x} \\in \\intg\\mid\\mathit{x} * \\mathit{x})$\n",
"* $\\mathit{r1} = 10000000000$"
],
"text/plain": [
@@ -35,7 +35,7 @@
"\n",
"Solution:\n",
"\tr2 = {1,4,9,16,25,36,49,64,81,100}\n",
- "\tf = /*@symbolic*/ λx·(x ∈ INTEGER∣x ∗ x)\n",
+ "\tf = /*@symbolic*/ λx·(x ∈ ℤ∣x ∗ x)\n",
"\tr1 = 10000000000"
]
},
@@ -65,18 +65,18 @@
{
"data": {
"text/markdown": [
- "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\mathit{TRUE}$\n",
+ "$\\def\\qdot{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\def\\intg{\\mathord{\\mathbb Z}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{r3} = \\{(1\\mapsto 4),(2\\mapsto 9),(3\\mapsto 25),(4\\mapsto 49),(5\\mapsto 121)\\}$\n",
- "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\lambda\\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid\\mathit{x} * \\mathit{x})$"
+ "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\lambda\\mathit{x}\\qdot(\\mathit{x} \\in \\intg\\mid\\mathit{x} * \\mathit{x})$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tr3 = {(1↦4),(2↦9),(3↦25),(4↦49),(5↦121)}\n",
- "\tf = /*@symbolic*/ λx·(x ∈ INTEGER∣x ∗ x)"
+ "\tf = /*@symbolic*/ λx·(x ∈ ℤ∣x ∗ x)"
]
},
"execution_count": 2,
@@ -104,18 +104,18 @@
{
"data": {
"text/markdown": [
- "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\mathit{TRUE}$\n",
+ "$\\def\\qdot{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\def\\intg{\\mathord{\\mathbb Z}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{r4} = 256$\n",
- "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\lambda\\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid\\mathit{x} * \\mathit{x})$"
+ "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\lambda\\mathit{x}\\qdot(\\mathit{x} \\in \\intg\\mid\\mathit{x} * \\mathit{x})$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tr4 = 256\n",
- "\tf = /*@symbolic*/ λx·(x ∈ INTEGER∣x ∗ x)"
+ "\tf = /*@symbolic*/ λx·(x ∈ ℤ∣x ∗ x)"
]
},
"execution_count": 3,
@@ -143,18 +143,18 @@
{
"data": {
"text/markdown": [
- "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\mathit{TRUE}$\n",
+ "$\\def\\qdot{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\def\\intg{\\mathord{\\mathbb Z}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{sqrt} = 10$\n",
- "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\lambda\\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid\\mathit{x} * \\mathit{x})$"
+ "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\lambda\\mathit{x}\\qdot(\\mathit{x} \\in \\intg\\mid\\mathit{x} * \\mathit{x})$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tsqrt = 10\n",
- "\tf = /*@symbolic*/ λx·(x ∈ INTEGER∣x ∗ x)"
+ "\tf = /*@symbolic*/ λx·(x ∈ ℤ∣x ∗ x)"
]
},
"execution_count": 4,
@@ -182,17 +182,17 @@
{
"data": {
"text/markdown": [
- "$\\newcommand{\\cprod}{\\mathbin\\times}\\newcommand{\\cprod}{\\mathbin\\times}\\mathit{TRUE}$\n",
+ "$\\def\\nat{\\mathord{\\mathbb N}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
- "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\{\\mathit{x},\\mathit{y}\\mid\\mathit{x} \\in \\mathit{NATURAL} \\land \\mathit{y} \\cprod 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) \\cprod 2 < \\mathit{x}\\}$\n",
+ "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\{\\mathit{x},\\mathit{y}\\mid\\mathit{x} \\in \\nat \\land \\mathit{y} ˄ 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) ˄ 2 < \\mathit{x}\\}$\n",
"* $\\mathit{r1} = 317$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
- "\tf = /*@symbolic*/ {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}\n",
+ "\tf = /*@symbolic*/ {x,y∣x ∈ ℕ ∧ y ˄ 2 ≥ x ∧ (y − 1) ˄ 2 < x}\n",
"\tr1 = 317"
]
},
@@ -221,14 +221,14 @@
{
"data": {
"text/markdown": [
- "$\\newcommand{\\cprod}{\\mathbin\\times}\\newcommand{\\cprod}{\\mathbin\\times}\\mathit{TRUE}$\n",
+ "$\\def\\nat{\\mathord{\\mathbb N}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{r2} = \\{1,2,3,4\\}$\n",
"* $\\mathit{r3} = \\{(1\\mapsto 2),(2\\mapsto 2),(3\\mapsto 3),(4\\mapsto 3),(5\\mapsto 4)\\}$\n",
"* $\\mathit{r4} = 2$\n",
"* $\\mathit{sqr} = 9802$\n",
- "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\{\\mathit{x},\\mathit{y}\\mid\\mathit{x} \\in \\mathit{NATURAL} \\land \\mathit{y} \\cprod 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) \\cprod 2 < \\mathit{x}\\}$\n",
+ "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\{\\mathit{x},\\mathit{y}\\mid\\mathit{x} \\in \\nat \\land \\mathit{y} ˄ 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) ˄ 2 < \\mathit{x}\\}$\n",
"* $\\mathit{r1} = 317$"
],
"text/plain": [
@@ -239,7 +239,7 @@
"\tr3 = {(1↦2),(2↦2),(3↦3),(4↦3),(5↦4)}\n",
"\tr4 = 2\n",
"\tsqr = 9802\n",
- "\tf = /*@symbolic*/ {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}\n",
+ "\tf = /*@symbolic*/ {x,y∣x ∈ ℕ ∧ y ˄ 2 ≥ x ∧ (y − 1) ˄ 2 < x}\n",
"\tr1 = 317"
]
},
@@ -272,18 +272,18 @@
{
"data": {
"text/markdown": [
- "$\\newcommand{\\cprod}{\\mathbin\\times}\\newcommand{\\cprod}{\\mathbin\\times}\\mathit{TRUE}$\n",
+ "$\\def\\nat{\\mathord{\\mathbb N}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{r5} = \\{2,4,10,100\\}$\n",
- "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\{\\mathit{x},\\mathit{y}\\mid\\mathit{x} \\in \\mathit{NATURAL} \\land \\mathit{y} \\cprod 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) \\cprod 2 < \\mathit{x}\\}$"
+ "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\{\\mathit{x},\\mathit{y}\\mid\\mathit{x} \\in \\nat \\land \\mathit{y} ˄ 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) ˄ 2 < \\mathit{x}\\}$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tr5 = {2,4,10,100}\n",
- "\tf = /*@symbolic*/ {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}"
+ "\tf = /*@symbolic*/ {x,y∣x ∈ ℕ ∧ y ˄ 2 ≥ x ∧ (y − 1) ˄ 2 < x}"
]
},
"execution_count": 7,
diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb
index 7b716bf0463fda3fa22f398542b1b8167e0a7de9..95705cbc0975675854d84e77b9e5051b4a515834 100644
--- a/notebooks/tutorials/prob_solver_intro.ipynb
+++ b/notebooks/tutorials/prob_solver_intro.ipynb
@@ -606,7 +606,7 @@
{
"data": {
"text/markdown": [
- "$\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\mathit{TRUE}$\n",
+ "$\\def\\upto{\\mathbin{.\\mkern1mu.}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{DOM} = (1 \\upto 9)$\n",
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 8ab0af3cbe01d4cefe2e4cfbcff3463d151f18e6..e41c4d46cf9331be2d6db0a23601519615d72f43 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -185,61 +185,61 @@ public final class ProBKernel extends BaseKernel {
private static final @NotNull Map<@NotNull String, @NotNull String> BSYMB_COMMAND_DEFINITIONS;
static {
final Map<String, String> map = new HashMap<>();
- map.put("bfalse", "\\newcommand{\\bfalse}{\\mathord\\bot}");
- map.put("btrue", "\\newcommand{\\btrue}{\\mathord\\top}");
- map.put("limp", "\\newcommand{\\limp}{\\mathbin\\Rightarrow}");
- map.put("leqv", "\\newcommand{\\leqv}{\\mathbin\\Leftrightarrow}");
- map.put("qdot", "\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}");
- map.put("defi", "\\newcommand{\\defi}{\\mathrel{≙}}");
- map.put("pow", "\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}");
- map.put("pown", "\\newcommand{\\pown}{\\mathop{\\mathbb P_1}\\nolimits}");
- map.put("cprod", "\\newcommand{\\cprod}{\\mathbin\\times}");
- map.put("bunion", "\\newcommand{\\bunion}{\\mathbin{\\mkern1mu\\cup\\mkern1mu}}");
- map.put("binter", "\\newcommand{\\binter}{\\mathbin{\\mkern1mu\\cap\\mkern1mu}}");
- map.put("union", "\\newcommand{\\union}{\\mathop{\\mathrm{union}}\\nolimits}");
- map.put("inter", "\\newcommand{\\inter}{\\mathop{\\mathrm{inter}}\\nolimits}");
- map.put("Union", "\\newcommand{\\Union}{\\bigcup\\nolimits}");
- map.put("Inter", "\\newcommand{\\Inter}{\\bigcap\\nolimits}");
- map.put("emptyset", "\\renewcommand{\\emptyset}{\\mathord\\varnothing}");
- map.put("rel", "\\newcommand{\\rel}{\\mathbin{<\\mkern-10mu-\\mkern-10mu>}}");
- map.put("trel", "\\newcommand{\\trel}{\\mathbin{<\\mkern-6mu<\\mkern-10mu-\\mkern-10mu>}}");
- map.put("srel", "\\newcommand{\\srel}{\\mathbin{<\\mkern-10mu-\\mkern-10mu>\\mkern-6mu>}}");
- map.put("strel", "\\newcommand{\\strel}{\\mathbin{<\\mkern-6mu<\\mkern-10mu-\\mkern-10mu>\\mkern-6mu>}}");
- map.put("dom", "\\newcommand{\\dom}{\\mathop{\\mathrm{dom}}\\nolimits}");
- map.put("ran", "\\newcommand{\\ran}{\\mathop{\\mathrm{ran}}\\nolimits}");
- map.put("fcomp", "\\newcommand{\\fcomp}{\\mathbin;}");
- map.put("bcomp", "\\newcommand{\\bcomp}{\\circ}");
- map.put("id", "\\newcommand{\\id}{\\mathop{\\mathrm{id}}\\nolimits}");
- map.put("domres", "\\newcommand{\\domres}{\\mathbin◁}");
- map.put("domsub", "\\newcommand{\\domsub}{\\mathbin⩤}");
- map.put("ranres", "\\newcommand{\\ranres}{\\mathbin▷}");
- map.put("ransub", "\\newcommand{\\ransub}{\\mathbin⩥}");
- map.put("ovl", "\\newcommand{\\ovl}{\\mathbin{<\\mkern-11mu+}}");
- map.put("dprod", "\\newcommand{\\dprod}{\\mathbin\\otimes}");
- map.put("prjone", "\\newcommand{\\prjone}{\\mathop{\\mathrm{prj}_1}\\nolimits}");
- map.put("prjtwo", "\\newcommand{\\prjtwo}{\\mathop{\\mathrm{prj}_2}\\nolimits}");
- map.put("pprod", "\\newcommand{\\pprod}{\\mathbin\\mid}");
- map.put("pfun", "\\newcommand{\\pfun}{\\mathbin↦}");
- map.put("tfun", "\\newcommand{\\tfun}{\\mathbin→}");
- map.put("pinj", "\\newcommand{\\pinj}{\\mathbin⤔}");
- map.put("tinj", "\\newcommand{\\tinj}{\\mathbin↣}");
- map.put("psur", "\\newcommand{\\psur}{\\mathbin⤅}");
- map.put("tsur", "\\newcommand{\\tsur}{\\mathbin↠}");
- map.put("tbij", "\\newcommand{\\tbij}{\\mathbin⤖}");
- map.put("nat", "\\newcommand{\\nat}{\\mathord{\\mathbb N}}");
- map.put("natn", "\\newcommand{\\natn}{\\mathord{\\mathbb N_1}}");
- map.put("intg", "\\newcommand{\\intg}{\\mathord{\\mathbb Z}}");
- map.put("upto", "\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}");
- map.put("finite", "\\newcommand{\\finite}{\\mathop{\\mathrm{finite}}\\nolimits}");
- map.put("card", "\\newcommand{\\card}{\\mathop{\\mathrm{card}}\\nolimits}");
- map.put("upred", "\\newcommand{\\upred}{\\mathop{\\mathrm{pred}}\\nolimits}");
- map.put("usucc", "\\newcommand{\\usucc}{\\mathop{\\mathrm{succ}}\\nolimits}");
- map.put("expn", "\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}");
- map.put("Bool", "\\newcommand{\\Bool}{\\mathord{\\mathrm{BOOL}}}");
- map.put("bool", "\\newcommand{\\bool}{\\mathop{\\mathrm{bool}}\\nolimits}");
- map.put("bcmeq", "\\newcommand{\\bcmeq}{\\mathrel{:\\mkern1mu=}}");
- map.put("bcmin", "\\newcommand{\\bcmin}{\\mathrel{:\\mkern1mu\\in}}");
- map.put("bcmsuch", "\\newcommand{\\bcmsuch}{\\mathrel{:\\mkern1mu\\mid}}");
+ map.put("bfalse", "\\def\\bfalse{\\mathord\\bot}");
+ map.put("btrue", "\\def\\btrue{\\mathord\\top}");
+ map.put("limp", "\\def\\limp{\\mathbin\\Rightarrow}");
+ map.put("leqv", "\\def\\leqv{\\mathbin\\Leftrightarrow}");
+ map.put("qdot", "\\def\\qdot{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}");
+ map.put("defi", "\\def\\defi{\\mathrel{≙}}");
+ map.put("pow", "\\def\\pow{\\mathop{\\mathbb P\\hbox{}}\\nolimits}");
+ map.put("pown", "\\def\\pown{\\mathop{\\mathbb P_1}\\nolimits}");
+ map.put("cprod", "\\def\\cprod{\\mathbin\\times}");
+ map.put("bunion", "\\def\\bunion{\\mathbin{\\mkern1mu\\cup\\mkern1mu}}");
+ map.put("binter", "\\def\\binter{\\mathbin{\\mkern1mu\\cap\\mkern1mu}}");
+ map.put("union", "\\def\\union{\\mathop{\\mathrm{union}}\\nolimits}");
+ map.put("inter", "\\def\\inter{\\mathop{\\mathrm{inter}}\\nolimits}");
+ map.put("Union", "\\def\\Union{\\bigcup\\nolimits}");
+ map.put("Inter", "\\def\\Inter{\\bigcap\\nolimits}");
+ map.put("emptyset", "\\def\\emptyset{\\mathord\\varnothing}");
+ map.put("rel", "\\def\\rel{\\mathbin{<\\mkern-10mu-\\mkern-10mu>}}");
+ map.put("trel", "\\def\\trel{\\mathbin{<\\mkern-6mu<\\mkern-10mu-\\mkern-10mu>}}");
+ map.put("srel", "\\def\\srel{\\mathbin{<\\mkern-10mu-\\mkern-10mu>\\mkern-6mu>}}");
+ map.put("strel", "\\def\\strel{\\mathbin{<\\mkern-6mu<\\mkern-10mu-\\mkern-10mu>\\mkern-6mu>}}");
+ map.put("dom", "\\def\\dom{\\mathop{\\mathrm{dom}}\\nolimits}");
+ map.put("ran", "\\def\\ran{\\mathop{\\mathrm{ran}}\\nolimits}");
+ map.put("fcomp", "\\def\\fcomp{\\mathbin;}");
+ map.put("bcomp", "\\def\\bcomp{\\circ}");
+ map.put("id", "\\def\\id{\\mathop{\\mathrm{id}}\\nolimits}");
+ map.put("domres", "\\def\\domres{\\mathbin◁}");
+ map.put("domsub", "\\def\\domsub{\\mathbin⩤}");
+ map.put("ranres", "\\def\\ranres{\\mathbin▷}");
+ map.put("ransub", "\\def\\ransub{\\mathbin⩥}");
+ map.put("ovl", "\\def\\ovl{\\mathbin{<\\mkern-11mu+}}");
+ map.put("dprod", "\\def\\dprod{\\mathbin\\otimes}");
+ map.put("prjone", "\\def\\prjone{\\mathop{\\mathrm{prj}_1}\\nolimits}");
+ map.put("prjtwo", "\\def\\prjtwo{\\mathop{\\mathrm{prj}_2}\\nolimits}");
+ map.put("pprod", "\\def\\pprod{\\mathbin\\mid}");
+ map.put("pfun", "\\def\\pfun{\\mathbin↦}");
+ map.put("tfun", "\\def\\tfun{\\mathbin→}");
+ map.put("pinj", "\\def\\pinj{\\mathbin⤔}");
+ map.put("tinj", "\\def\\tinj{\\mathbin↣}");
+ map.put("psur", "\\def\\psur{\\mathbin⤅}");
+ map.put("tsur", "\\def\\tsur{\\mathbin↠}");
+ map.put("tbij", "\\def\\tbij{\\mathbin⤖}");
+ map.put("nat", "\\def\\nat{\\mathord{\\mathbb N}}");
+ map.put("natn", "\\def\\natn{\\mathord{\\mathbb N_1}}");
+ map.put("intg", "\\def\\intg{\\mathord{\\mathbb Z}}");
+ map.put("upto", "\\def\\upto{\\mathbin{.\\mkern1mu.}}");
+ map.put("finite", "\\def\\finite{\\mathop{\\mathrm{finite}}\\nolimits}");
+ map.put("card", "\\def\\card{\\mathop{\\mathrm{card}}\\nolimits}");
+ map.put("upred", "\\def\\upred{\\mathop{\\mathrm{pred}}\\nolimits}");
+ map.put("usucc", "\\def\\usucc{\\mathop{\\mathrm{succ}}\\nolimits}");
+ map.put("expn", "\\def\\expn{\\mathbin{\\widehat{\\mkern1em}}}");
+ map.put("Bool", "\\def\\Bool{\\mathord{\\mathrm{BOOL}}}");
+ map.put("bool", "\\def\\bool{\\mathop{\\mathrm{bool}}\\nolimits}");
+ map.put("bcmeq", "\\def\\bcmeq{\\mathrel{:\\mkern1mu=}}");
+ map.put("bcmin", "\\def\\bcmin{\\mathrel{:\\mkern1mu\\in}}");
+ map.put("bcmsuch", "\\def\\bcmsuch{\\mathrel{:\\mkern1mu\\mid}}");
BSYMB_COMMAND_DEFINITIONS = Collections.unmodifiableMap(map);
}