equal
deleted
inserted
replaced
326 described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will |
326 described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will |
327 give directions identified for future development. |
327 give directions identified for future development. |
328 |
328 |
329 |
329 |
330 \section{\isac's Prototype for a Programming Language}\label{PL} |
330 \section{\isac's Prototype for a Programming Language}\label{PL} |
331 The prototype of the language and of the Lucas-Interpreter are briefly |
331 The prototype of the language and of the Lucas-Interpreter is briefly |
332 described from the point of view of a programmer. The language extends |
332 described from the point of view of a programmer. The language extends |
333 the executable fragment in the language of the theorem prover |
333 the executable fragment in the language of the theorem prover |
334 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}. |
334 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}. |
335 |
335 |
336 \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab} |
336 \subsection{The Executable Fragment of Isabelle's Language}\label{PL-isab} |