]> matita.cs.unibo.it Git - helm.git/commitdiff
* version with single continuation
authorLuca Padovani <luca.padovani@unito.it>
Sun, 6 Apr 2003 07:47:41 +0000 (07:47 +0000)
committerLuca Padovani <luca.padovani@unito.it>
Sun, 6 Apr 2003 07:47:41 +0000 (07:47 +0000)
helm/DEVEL/mathml_editor/doc/spec.tex

index 87e2cd603a2817b34689fdb559c9a4dc2519db8e..c99c659090dd7d5bdaf7f91967aa60624436a07c 100644 (file)
@@ -932,15 +932,15 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
   \PSEM{c_1\mid c_2} &=& \FUN{x}{(\PSEM{c_1}\;x)\vee(\PSEM{c_2}\;x)}\\
   \PSEM{c+} &=& \PSEM{c}\\
   \PSEM{c?} &=& \FUN{\_}{\TRUE}\\
-  \PSEM{c*} &=& \FUN{\_}{\TRUE}\\
-  \PSEM{!c} &=& \FUN{x}{\neg(\PSEM{c}\;x)}\\[3ex]
+  \PSEM{c*} &=& \FUN{\_}{\TRUE}\\[3ex]
   \FSEM{q}{l} &=& \FUN{x}{\IFH{(\PSEM{q}\;x)}{(l\;x)}{\FALSE}}\\
   \FSEM{..}{l} &=& \FUN{x}{\IFH{\PARENT{x}=\{y\}}{(l\;y)}{\FALSE}}\\
   \FSEM{/}{l} &=& \FUN{x}{\vee_{p\in\CHILDREN{x}} (l\;p)}\\
-  \FSEM{c_1\;c_2}{l} &=& \FUN{x}{(\FSEM{c_1}{\FSEM{c_2}{l}}\;x)}\\
-  \FSEM{c_1\&c_2}{l} &=& \FUN{x}{(\FSEM{c_1}{\FUN{y}{\IFH{(l\;y)}{(\FSEM{c_2}{\FUN{z}{z=y}}\;x)}{\FALSE}}}\;x)}\\
+  \FSEM{(c)}{l} &=& \FSEM{c}{l}\\
+  \FSEM{c_1\;c_2}{l} &=& \FSEM{c_1}{\FSEM{c_2}{l}}\\
+  \FSEM{c_1\&c_2}{l} &=& \FUN{x}{(\FSEM{c_1}{\FUN{y}{(l\;y)\wedge(\FSEM{c_2}{\FUN{z}{z=y}}\;x)}}\;x)}\\
   \FSEM{c_1\mid c_2}{l} &=& \FUN{x}{(\FSEM{c_1}{l}\;x)\vee(\FSEM{c_2}{l}\;x)}\\
-  \FSEM{c+}{l} &=& \FUN{x}{(\FSEM{c}{\FUN{y}{(l\;y)\vee(\FSEM{c+}{l}\;y)}}\;x)}\\
+  \FSEM{c+}{l} &=& \FSEM{c}{\FUN{y}{(l\;y)\vee(\FSEM{c+}{l}\;y)}}\\
   \FSEM{c?}{l} &=& \FUN{x}{(l\;x)\vee(\FSEM{c}{l}\;x)}\\
   \FSEM{c*}{l} &=& \FSEM{{c+}?}{l}\\
 \end{array}