# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1309366582 -7200
# Node ID 3402f14d907a0e0d4a76ca2bba7b34effc06ce6b
# Parent  241e7ad6593c4d7886300e55cb362399f02357f1
Layout and stuff.

diff -r 241e7ad6593c -r 3402f14d907a paper/src/paper.tex
--- a/paper/src/paper.tex	Wed Jun 29 18:39:07 2011 +0200
+++ b/paper/src/paper.tex	Wed Jun 29 18:56:22 2011 +0200
@@ -175,7 +175,7 @@
 
 \subsection{Semantics}
 \begin{def:frames}
-A LTL-\emph{frame} is a tuple $\F = (S, R)$, where $S = \{s_i \mid i \in \N\}$ is the set of states and $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ the set of accessibility relations. Hence $S$ is an isomorphism of $\N$ and $R$ an isomorphism of the strict linear order $(\N, <)$, which corresponds to the linear progression of time. 
+A LTL-\emph{frame} is a tuple $\F = (S, R)$, where $S = \{s_i \mid i \in \N\}$ is the set of states and $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ the set of accessibility relations. Hence $S$ is an isomorphism of $\N$ and $R$ an isomorphism of the strict linear order $(\N, <)$, which corresponds to the linear progression of discrete time. 
 \end{def:frames}
 
 \begin{def:models}