1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Oct 14 21:35:45 2012 +0200
     1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Tue Oct 30 21:07:44 2012 +0100
     1.3 @@ -209,8 +209,8 @@
     1.4  programming language''. In the
     1.5  {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such
     1.6  a language is prototyped in line with~\cite{plmms10} and built upon
     1.7 -the theorem prover.
     1.8 -Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}.
     1.9 +the theorem prover Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}
    1.10 +\footnote{http://isabelle.in.tum.de/}.
    1.11  The TP services are coordinated by a specific interpreter for the
    1.12  programming language, called
    1.13  Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the
    1.14 @@ -224,16 +224,16 @@
    1.15  Telematics (computer science with focus on Signal Processing) he had
    1.16  general knowledge in programming as well as specific domain knowledge
    1.17  in Signal Processing; and he was {\em not} involved in the development of
    1.18 -{\sisac}'s programming language and interpreter, thus a novice to the
    1.19 +{\sisac}'s programming language and interpreter, thus being a novice to the
    1.20  language.
    1.21  
    1.22 -The goal of the case study was (1) some TP-based programs for
    1.23 +The goals of the case study were: (1) to identify some TP-based programs for
    1.24  interactive course material for a specific ``Advanced Signal
    1.25  Processing Lab'' in a higher semester, (2) respective program
    1.26 -development with as little advice from the {\sisac}-team and (3) records
    1.27 -and comments for the main steps of development in an Isabelle theory;
    1.28 -this theory should provide guidelines for future programmers. An
    1.29 -excerpt from this theory is the main part of this paper.
    1.30 +development with as little advice as possible from the {\sisac}-team and (3) 
    1.31 +to document records and comments for the main steps of development in an
    1.32 +Isabelle theory; this theory should provide guidelines for future programmers.
    1.33 +An excerpt from this theory is the main part of this paper.
    1.34  \par
    1.35  The paper will use the problem in Fig.\ref{fig-interactive} as a
    1.36  running example:
    1.37 @@ -277,7 +277,7 @@
    1.38  mathematics-authors (in Isabelle/ML); their task is concern of this
    1.39  paper.
    1.40  
    1.41 -\paragraph{The paper is structured} as follows: The introduction
    1.42 +The paper is structured as follows: The introduction
    1.43  \S\ref{intro} is followed by a brief re-introduction of the TP-based
    1.44  programming language in \S\ref{PL}, which extends the executable
    1.45  fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which
    1.46 @@ -301,8 +301,8 @@
    1.47  \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab}
    1.48  The executable fragment consists of data-type and function
    1.49  definitions.  It's usability even suggests that fragment for
    1.50 -introductory courses \cite{nipkow-prog-prove}. HOL is a typed logic
    1.51 -whose type system resembles that of functional programming
    1.52 +introductory courses \cite{nipkow-prog-prove}. HOL (Higher-Order Logic)
    1.53 +is a typed logic whose type system resembles that of functional programming
    1.54  languages. Thus there are
    1.55  \begin{description}
    1.56  \item[base types,] in particular \textit{bool}, the type of truth
    1.57 @@ -369,7 +369,7 @@
    1.58  
    1.59  \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}
    1.60  The prototype extends Isabelle's language by specific statements
    1.61 -called tactics~\footnote{{\sisac}'s tactics are different from
    1.62 +called tactics~\footnote{{\sisac}'s. This tactics are different from
    1.63  Isabelle's tactics: the former concern steps in a calculation, the
    1.64  latter concern proofs.}  and tactics. For the programmer these
    1.65  statements are functions with the following signatures:
    1.66 @@ -846,7 +846,7 @@
    1.67  09   *}
    1.68  \end{verbatim}}
    1.69  
    1.70 -\noindent The function body creates either creates \texttt{NONE}
    1.71 +\noindent The function body creates either \texttt{NONE}
    1.72  telling the rewrite-engine to search for the next redex, or creates an
    1.73  ad-hoc theorem for rewriting, thus the programmer needs to adopt many
    1.74  technicalities of Isabelle, for instance, the \textit{Trueprop}
    1.75 @@ -1273,8 +1273,7 @@
    1.76  
    1.77  \medskip The above program also indicates the dominant role of interactive
    1.78  selection of knowledge in the three-dimensional universe of
    1.79 -mathematics as depicted in Fig.\ref{fig:mathuni} on
    1.80 -p.\pageref{fig:mathuni}, The \texttt{SubProblem} in the above lines
    1.81 +mathematics. The \texttt{SubProblem} in the above lines
    1.82  {\rm 07..09} is more than a function call with the actual arguments
    1.83  \textit{[ (rhs X\_eq)::real, z::real ]}. The programmer has to determine
    1.84  three items: