From: Luca Padovani <luca.padovani@unito.it>
Date: Sun, 6 Apr 2003 07:47:41 +0000 (+0000)
Subject: * version with single continuation
X-Git-Tag: before_refactoring~47
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7bbc3826e7478e46a0802334cd1befa7d65e60db;p=helm.git

* version with single continuation
---

diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex
index 87e2cd603..c99c65909 100644
--- a/helm/DEVEL/mathml_editor/doc/spec.tex
+++ b/helm/DEVEL/mathml_editor/doc/spec.tex
@@ -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}