\author[Lehnfeld, Neuper] % (optional, use only with lots of authors)

 \author[Lehnfeld] % (optional, use only with lots of authors)

 {Mathias~Lehnfeld\inst{1} \and Walther~Neuper\inst{2}}

 {Mathias~Lehnfeld}

   \inst{1}%

   Vienna University of Technology\\

   Vienna University of Technology

   Institute of Computer Languages

   \and

   \inst{2}%

   Institute of Software Technology\\

   Graz University of Technology

 \subsection[TODO]{Isabelle and \isac}

 \subsection[Isabelle \& \isac]{Isabelle and \isac}

 TODO

     \begin{itemize}

 \end{frame}

     \item Computer Theorem Prover Isabelle

     \item Math Learning Assistent \isac

 \subsection[TODO]{Computation and deduction in a Lucas-Interpreter}

     \end{itemize}

 \begin{frame}

 \end{frame}

   \frametitle{Computation and deduction in a Lucas-Interpreter}

 TODO

 \subsection[Computation \& Deduction]{Computation and Deduction in a Lucas-Interpreter}

 \begin{frame}

   \frametitle{Computation and Deduction in a Lucas-Interpreter}

     \includegraphics[width=100mm]{overview.pdf}

 \subsection[TODO]{Introduction of Isabelle Contexts}

 \subsection[Contexts]{Introduction of Isabelle Contexts}

 \begin{frame}

 \begin{frame}

   \frametitle{TODO}

   \frametitle{Introduction of Isabelle Contexts}

 TODO

     \begin{itemize}

 \end{frame}

     \item theories too general

     \item not capable of type inference

 \subsection[TODO]{Redesign of type inference in \isac}

     \item replace function \texttt{parseNEW}

 \begin{frame}

     \end{itemize}

   \frametitle{TODO}

 \end{frame}

 TODO

 \end{frame}

 \begin{frame}

   \frametitle{Introduction of Isabelle Contexts}

 \subsection[TODO]{Improvement of functional code}

     \texttt{\tiny{

 \begin{frame}

       \begin{tabbing}

   \frametitle{Drop \textit{Check\_Elementwise} !}

 xx\=xx\=xx\=xx\=\kill

 %\begin{verbatim}

 fun parse thy str =\\

 %solve (x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 / x, x)

 \>(let val t = (typ\_a2real o numbers\_to\_string)\\

 %   x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 / x

 \>\>\>\>(Syntax.read\_term\_global thy str)\\

 %   x / (x ^ 2 + -1 * (6 * x) + 9) + -1 * 1 / (x ^ 2 + -1 * (3 * x)) = 1 / x

 \>\>in SOME (cterm\_of thy t) end)\\

 %   (3 + -1 * x + x ^ 2) / (9 * x + -6 * x ^ 2 + x ^ 3) = 1 / x

 \>\>\>handle \_ => NONE;

 %   (3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)

 \\~\\~\\

 %   solve ((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)

 fun parseNEW ctxt str = SOME (Syntax.read\_term ctxt str |> numbers\_to\_string)\\

 %      (3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)

 \>\>\>handle \_ => NONE;

 %      (3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0

 \\~\\~\\

 %      (3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0

 local\\

 %      -6 * x + 5 * x ^ 2 = 0

 \>fun insert\_ctxt data = ContextData.map (fn xs => distinct (data@xs));\\

 %      solve (-6 * x + 5 * x ^ 2 = 0, x)

 in\\

 %      [x = 0, x = 6 / 5]

 \>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\

 %   [x = 0, x = 6 / 5]

 \>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\

 %   [x = 6 / 5]

 end

 %[x = 6 / 5]

       \end{tabbing}

 %\end{verbatim}

     }}

 \end{frame}

 \subsection[Redesign]{Redesign of Type Inference in \isac}

 \begin{frame}

   \frametitle{Redesign of type inference in \isac}

     \begin{itemize}

     \item use context type inference

     \item parsing input (specification \& user input)

     \item specification with polymorphic types

     \item etc.

     \end{itemize}

 \end{frame}

 \subsection[Code Improvement]{Improvement of functional code}

 \begin{frame}

   \frametitle{Improvement of functional code}

   \begin{itemize}

   \item combinators

   \item code conventions

   \end{itemize}

 \end{frame}

 \begin{frame}

   \frametitle{Combinators \& Code Conventions}

     \texttt{\tiny{

       \begin{tabbing}

 xx\=xx\=xx\=xx\=xx\=\kill

 fun prep\_ori [] \_ \_ = ([], e\_ctxt)\\

 \>| prep\_ori fmz thy pbt =\\

 \>\>\>let\\

 \>\>\>\>val ctxt = ProofContext.init\_global thy |> fold declare\_constraints fmz\\

 \>\>\>\>val ori = map (add\_field thy pbt o split\_dts o the o parseNEW ctxt) fmz\\

 \>\>\>\>\>|> add\_variants\\

 \>\>\>\>val maxv = map fst ori |> max\\

 \>\>\>\>val maxv = if maxv = 0 then 1 else maxv\\

 \>\>\>\>val oris = coll\_variants ori\\

 \>\>\>\>\>|> map (replace\_0 maxv |> apfst)\\

 \>\>\>\>\>|> add\_id\\

 \>\>\>\>\>|> map flattup\\

 \>\>\>in (oris, ctxt) end;

       \end{tabbing}

     }}

 \end{frame}

 \begin{frame}

   \frametitle{Drop \tt{Check\_Elementwise}!}

 \subsection[TODO]{Preparation of future development}

 \subsection[Future Development]{Preparation of Future Development}

 \begin{frame}

 \begin{frame}

   \frametitle{TODO}

   \frametitle{Preparation of Future Development}

     \begin{itemize}

     \item logical data for Isabelle provers in contexts

     \item \isac programming language more compact\\

       $\rightarrow$ context built automatically

     \end{itemize}

 \end{frame}

 \section[Problems]{Problems encountered in the project}

 \begin{frame}

   \frametitle{Problems encountered in the project}

     \begin{itemize}

     \item publication of new Isabelle release

     \item amount of code in Isabelle and \isac

     \item changes scattered throughout the code

     \end{itemize}

 \end{frame}

 \section{Summary}

 \begin{frame}

   \frametitle{Summary}