diff options
Diffstat (limited to 'papers/cfrontend_new/trace.etex')
-rw-r--r-- | papers/cfrontend_new/trace.etex | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/papers/cfrontend_new/trace.etex b/papers/cfrontend_new/trace.etex deleted file mode 100644 index d02b1fe9..00000000 --- a/papers/cfrontend_new/trace.etex +++ /dev/null @@ -1,19 +0,0 @@ -\begin{figure} - -\begin{syntax} -\syntaxclass{Event values:} -\evv & ::= & n & integer value\\ - & \alt & f & floating-point value -% -\syntaxclass{Events:} -\ev & ::= & \id \, \evv^* \, \evv & -% -\syntaxclass{Execution traces:} -\tr & ::= & \E0 & empty trace \\ - & \alt & [\ev] & external call \\ - & \alt & \cat \tr \tr& concatenation -\end{syntax} -\caption{Execution traces} -\label{fig:trace} -\end{figure} - |