1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Fri Nov 02 16:28:13 2012 +0100
     1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Fri Nov 02 18:07:12 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  

     2.1 --- a/doc-src/isac/jrocnik/eJMT-paper/references.bib	Fri Nov 02 16:28:13 2012 +0100
     2.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/references.bib	Fri Nov 02 18:07:12 2012 +0100
     2.3 @@ -1,3 +1,11 @@
     2.4 +@Misc{coq-team-10,
     2.5 +  author = 	 {Coq development team},
     2.6 +  title = 	 {Coq 8.3 Reference Manual},
     2.7 +  howpublished = {http://coq.inria.fr/reman},
     2.8 +  year = 	 {2010},
     2.9 +  note = 	 {INRIA}
    2.10 +}
    2.11 +
    2.12  @Book{db:dom-eng,
    2.13    author = 	 {Bj{\o}rner, Dines},
    2.14    title = 	 {Domain Engineering. Technology Management, Research and Engineering},