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 16:28:13 2012 +0100
     1.3 @@ -251,16 +251,16 @@
     1.4  http://www.ist.tugraz.at/projects/isac/www/kbase/met/index\_met.html})
     1.5  
     1.6  \paragraph{The mathematical background of the running example} is the
     1.7 -following: In Signal Processing, ``the ${\cal Z}$-Transform for
     1.8 +following: In Signal Processing, ``the ${\cal Z}$-transform for
     1.9  discrete-time signals is the counterpart of the Laplace transform for
    1.10  continuous-time signals, and they each have a similar relationship to
    1.11  the corresponding Fourier transform. One motivation for introducing
    1.12  this generalization is that the Fourier transform does not converge
    1.13  for all sequences, and it is useful to have a generalization of the
    1.14  Fourier transform that encompasses a broader class of signals. A
    1.15 -second advantage is that in analytic problems, the $z$-transform
    1.16 +second advantage is that in analytic problems, the ${\cal Z}$-transform
    1.17  notation is often more convenient than the Fourier transform
    1.18 -notation.''  ~\cite[p. 128]{oppenheim2010discrete}.  The $z$-transform
    1.19 +notation.''  ~\cite[p. 128]{oppenheim2010discrete}.  The ${\cal Z}$-transform
    1.20  is defined as
    1.21  \begin{equation*}
    1.22  X(z)=\sum_{n=-\infty }^{\infty }x[n]z^{-n}
    1.23 @@ -273,9 +273,9 @@
    1.24  x[n]=\frac{1}{2\pi j} \oint_{C} X(z)\cdot z^{n-1} dz
    1.25  \end{equation*}
    1.26  where the letter $C$ represents a contour within the range of
    1.27 -convergence of the $z$- transform. The unit circle can be a special
    1.28 +convergence of the ${\cal Z}$-transform. The unit circle can be a special
    1.29  case of this contour. Remember that $j$ is the complex number in the
    1.30 -domain of engineering.  As this transformation requires high effort to
    1.31 +domain of engineering.  As this transform requires high effort to
    1.32  be solved, tables of commonly used transform pairs are used in
    1.33  education as well as in engineering practice; such tables can be found
    1.34  at~\cite{wiki:1} or~\cite[Table~3.1]{oppenheim2010discrete} as well.
    1.35 @@ -705,8 +705,8 @@
    1.36  % allows to omit proofs. Such a theorem is shown in
    1.37  % Example~\ref{eg:neuper1}.
    1.38  
    1.39 -The running example requires to determine the inverse $\cal
    1.40 -Z$-transform for a class of functions. The domain of Signal Processing
    1.41 +The running example requires to determine the inverse ${\cal Z}$-transform
    1.42 +for a class of functions. The domain of Signal Processing
    1.43  is accustomed to specific notation for the resulting functions, which
    1.44  are absolutely capable of being totalled and are called step-response: $u[n]$, where $u$ is the
    1.45  function, $n$ is the argument and the brackets indicate that the
    1.46 @@ -731,8 +731,8 @@
    1.47  % \end{example}
    1.48  %}
    1.49  These 6 rules can be used as conditional rewrite rules, depending on
    1.50 -the respective convergence radius. Satisfaction from accordance with traditional notation
    1.51 -contrasts with the above word {\em axiomatization}: As TP-based, the
    1.52 +the respective convergence radius. Satisfaction from accordance with traditional
    1.53 +notation contrasts with the above word {\em axiomatization}: As TP-based, the
    1.54  programming language expects these rules as {\em proved} theorems, and
    1.55  not as axioms implemented in the above brute force manner; otherwise
    1.56  all the verification efforts envisaged (like proof of the
    1.57 @@ -741,7 +741,7 @@
    1.58  Isabelle provides a large body of knowledge, rigorously proved from
    1.59  the basic axioms of mathematics~\footnote{This way of rigorously
    1.60  deriving all knowledge from first principles is called the
    1.61 -LCF-paradigm in TP.}. In the case of the ${\cal Z}$-Transform the most advanced
    1.62 +LCF-paradigm in TP.}. In the case of the ${\cal Z}$-transform the most advanced
    1.63  knowledge can be found in the theories on Multivariate
    1.64  Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However,
    1.65  building up knowledge such that a proof for the above rules would be
    1.66 @@ -2048,8 +2048,8 @@
    1.67  which is considered a standard normal form in Computer Algebra.
    1.68  \item Implement a specification for partial fraction decomposition and
    1.69  locate it appropriately in the hierarchy of specification.
    1.70 -\item Declare definitions and theorems within the theory of ${\cal
    1.71 -Z}$-Transformation, and prove the theorems (which was not done in the
    1.72 +\item Declare definitions and theorems within the theory of
    1.73 +${\cal Z}$-transform, and prove the theorems (which was not done in the
    1.74  case study).
    1.75  \end{itemize}
    1.76  On the other hand, for the one the class of problems implemented,