1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Fri Nov 02 13:06:16 2012 +0100
     1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Fri Nov 02 18:06:54 2012 +0100
     1.3 @@ -290,7 +290,7 @@
     1.4  the lack of 2-dimensional presentation and input of formulas is the major obstacle for field-tests in standard classes.}:
     1.5  A student inputs formulas line by line on the \textit{``Worksheet''},
     1.6  and each step (i.e. each formula on completion) is immediately checked
     1.7 -by the system such that at most one inconsistent formula can reside on
     1.8 +by the system, such that at most {\em one inconsistent} formula can reside on
     1.9  the Worksheet (on the input line, marked by the red $\otimes$).
    1.10  \begin{figure} [htb]
    1.11  \begin{center}
    1.12 @@ -450,9 +450,9 @@
    1.13  
    1.14  \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
    1.15  The prototype extends Isabelle's language by specific statements
    1.16 -called tactics~\footnote{{\sisac}'s. This tactics are different from
    1.17 +called tactics~\footnote{{\sisac}'s. These tactics are different from
    1.18  Isabelle's tactics: the former concern steps in a calculation, the
    1.19 -latter concern proofs.}  and tactics. For the programmer these
    1.20 +latter concern proofs.}. For the programmer these
    1.21  statements are functions with the following signatures:
    1.22  
    1.23  \begin{description}
    1.24 @@ -2111,7 +2111,7 @@
    1.25  one side inreasing demand for formal domain engineering and from the
    1.26  other side from TP more and more gaining industrial relevance. Within
    1.27  this window, development of TP-based educational software can take
    1.28 -benefit from the fact, that the TPs leading in Europe, Coq and
    1.29 +benefit from the fact, that the TPs leading in Europe, Coq~\cite{coq-team-10} and
    1.30  Isabelle are still open source together with the major part of
    1.31  mechanised knowledge.%~\footnote{NICTA}.
    1.32