Commit 71a260c2 by Michael Kohlhase

### changing

 \begin{modnl}[creators=miko]{abstract-reduction-system}{en} \begin{mhmodnl}[creators=miko]{abstract-reduction-system}{en} \begin{definition} An \defiii{abstract}{reduction}{system} (or \defiii[abstract-reduction-system]{abstract}{rewriting}{system}, or ... ... @@ -10,7 +10,7 @@ denoted by $\arsconvtrOp$. To distinguish the original relation $\arsconvOp$ it is sometimes written as $\arsconvOp[1]$. \end{definition} \end{modnl} \end{mhmodnl} %%% Local Variables: %%% mode: latex %%% TeX-master: t ... ...
 \begin{modnl}[creators=miko]{alpharenaming}{de} \begin{mhmodnl}[creators=miko]{alpharenaming}{de} \begin{definition} Wir nennen eine Formel $\bA$ eine \defii[alphabetic-variant]{alphabetische}{Variante} von $\bB$ (oder \adefii[alphabetic-variant]{$\alphaeqRel$-gleich}{alpha}{gleich}; schreibe $\alphaeq\bA\bB$), wenn $\bB$ aus $\bA$ hervorgeht durch systematische Umbenennung gebundener Variablen. \end{definition} \end{modnl} \end{mhmodnl} %%% Local Variables: %%% mode: latex %%% TeX-master: t ... ...
 \begin{modnl}[creators=jusche]{alpharenaming}{en} \begin{mhmodnl}[creators=jusche]{alpharenaming}{en} \begin{definition} We call a formula $\bA$ an \defii{alphabetic}{variant} of $\bB$ (or \adefii[alphabetic-variant]{$\alphaeqRel$-equal}{alpha}{equal}; write $\alphaeq\bA\bB$), iff $\bB$ can be obtained from $\bA$ by systematically renaming bound variables. \end{definition} \end{modnl} \end{mhmodnl} %%% Local Variables: %%% mode: latex %%% TeX-master: t ... ...
 \begin{modnl}[creators=miko]{confluent}{en} \begin{mhmodnl}[creators=miko]{confluent}{en} \begin{definition}[title=Confluence,id=confluent.def] We say that an \trefiii[abstract-reduction-system]{abstract}{reduction}{system} $\mvstructure{A,R}$ ... ... @@ -51,7 +51,7 @@ \end{tabular} \end{center} \end{definition} \end{modnl} \end{mhmodnl} %%% Local Variables: %%% mode: latex %%% TeX-master: t ... ...