LMCS-Paper/Paper.thy
changeset 3014 e57c175d9214
parent 3013 01a3861035d4
child 3015 4fafa8d219dc
equal deleted inserted replaced
3013:01a3861035d4 3014:e57c175d9214
  1292 
  1292 
  1293   The first non-trivial step we have to perform is the generation of
  1293   The first non-trivial step we have to perform is the generation of
  1294   \emph{free-atom functions} from the specifications.\footnote{Admittedly, the
  1294   \emph{free-atom functions} from the specifications.\footnote{Admittedly, the
  1295   details of our definitions will be somewhat involved. However they are still
  1295   details of our definitions will be somewhat involved. However they are still
  1296   conceptually simple in comparison with the ``positional'' approach taken in
  1296   conceptually simple in comparison with the ``positional'' approach taken in
  1297   Ott \cite[Pages 88--95]{ott-jfp}, which uses the notions of \emph{occurences} and
  1297   Ott \cite[Pages 88--95]{ott-jfp}, which uses the notions of \emph{occurrences} and
  1298   \emph{partial equivalence relations} over sets of occurences.} For the
  1298   \emph{partial equivalence relations} over sets of occurrences.} For the
  1299   \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
  1299   \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
  1300 
  1300 
  1301   \begin{equation}\label{fvars}
  1301   \begin{equation}\label{fvars}
  1302   \mbox{@{text "fa_ty"}$_{1..n}$}
  1302   \mbox{@{text "fa_ty"}$_{1..n}$}
  1303   \end{equation}\smallskip
  1303   \end{equation}\smallskip