
neuper@41965: % /usr/share/doc/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex
neuper@41965: 
neuper@41965: \documentclass{beamer}
neuper@41965: \mode<presentation>
neuper@41965: {
neuper@41965:   \usetheme{Hannover}
neuper@41965:   \setbeamercovered{transparent}
neuper@41965: }
neuper@41965: \usepackage[english]{babel}
neuper@41965: \usepackage[latin1]{inputenc}
neuper@41965: \usepackage{times}
neuper@42042: \usepackage{ngerman}
neuper@41965: \usepackage[T1]{fontenc}
neuper@41965: %\usepackage{graphicx}
neuper@41965: 
neuper@41965: \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
neuper@41965: \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
neuper@41965: 
neuper@41965: \title[Isabelle Frontend]
neuper@41965: {Userinterfaces \\f\"ur Computer Theorem Prover,\\
neuper@42042: 	Machbarkeits-Studie im \isac-Projekt
neuper@41965: }
neuper@41965: \subtitle{Bachelorarbeit Telematik}
neuper@41965: 
neuper@41965: \author{Marco Steger}
neuper@41965: \institute{Institut f\"ur Software Technologie\\
neuper@41965:   Technische Universit\"at Graz}
neuper@41965: 
m@42049: \date{21.06.2011}
neuper@41965: %\subject{Formal specification of math assistants}
neuper@41965: % This is only inserted into the PDF information catalog
neuper@41965: 
neuper@41965: % Delete this, if you do not want the table of contents to pop up at
neuper@41965: % the beginning of each subsection:
neuper@41965: \AtBeginSubsection[]
neuper@41965: {
neuper@41965:   \begin{frame}<beamer>
neuper@41965:     \frametitle{Outline}
neuper@41965:     \tableofcontents[currentsection,currentsubsection]
neuper@41965:   \end{frame}
neuper@41965: }
neuper@41965: 
neuper@41965: 
neuper@41965: % If you wish to uncover everything in a step-wise fashion, uncomment
neuper@41965: % the following command: 
neuper@41965: %\beamerdefaultoverlayspecification{<+->}
neuper@41965: 
neuper@41965: 
neuper@41965: \begin{document}
neuper@41965: \begin{frame}
neuper@41965:   \titlepage
neuper@41965: \end{frame}
neuper@41965: 
neuper@41965: \begin{frame}
neuper@41965:   \frametitle{Outline}
neuper@41965:   \tableofcontents
neuper@41965:   % You might wish to add the option [pausesections]
neuper@41965: \end{frame}
neuper@41965: 
neuper@42046: \section[Stutus quo]{Ausgangssituation: das k\"unftige Isabelle Front-end}
neuper@42046: \subsection[Isabelle]{Der Theoremprover Isabelle}
neuper@41965: \begin{frame}
neuper@41965:   \frametitle{Der Theoremprover Isabelle}
neuper@41965: \begin{itemize}
neuper@41965: \item Anwendungen von Isabelle
neuper@41965:   \begin{itemize}
neuper@41965:   \item Mechanisieren von Mathematik Theorien
neuper@41965:     \begin{itemize}
neuper@41965:     \item nat\"urliche, reelle, komplexe Zahlen, Listen, Lattices, \dots
neuper@41965:     \item Gr\"obner Basen, Integral/Differential, Taylorreihen, \dots          
neuper@41965:     \item High Order Logics, Logic of Computable Functions, \dots
neuper@41965:     \end{itemize}
neuper@42042: \pause
neuper@41965:   \item Math.Grundlagen f\"ur Softwaretechnologie
neuper@41965:     \begin{itemize}
neuper@41965:     \item Hoare Logic, Temporal Logic of Actions, Hoare for Java
neuper@41965:     \item Theory for Unix file-system security, for state spaces, \dots
neuper@41965:     \item Archive of Formal Proofs {\tiny\tt http://afp.sourceforge.net}
neuper@41965:     \end{itemize}
neuper@41965:   \end{itemize}
neuper@42042: \pause
neuper@41965: \item Integration von Isabelle in Entwicklungstools
neuper@41965:   \begin{itemize}
neuper@41965:   \item Boogie --- Verification Condition Generator
neuper@42042:   \item $\mathbf{\pi}d.e$ Projekt: Unterst\"utzung Domain-spezifischen CTPs
neuper@42042:   \item Test Case Generators (TUG) ?
neuper@41965:   \end{itemize}
neuper@42042: \pause
neuper@41965: \item Isar, die Beweissprache von Isabelle
neuper@42042:   \begin{itemize}
m@42049:   %\item Demo $\sqrt{2}\not\in{\cal R}\;\;\;$ 
m@42049:   \item Demo 'Allgemeine Dreiecke'
neuper@41965: \pause
neuper@42042: \alert{Beweisteile asynchron interpretiert}
neuper@41965:   \end{itemize}
neuper@41965: \end{itemize}
neuper@41965: \end{frame}
neuper@41965: 
neuper@42042: \subsection[Scala-Layer]{Die Konzeption des Scala-Layers}
neuper@42042: \begin{frame}\frametitle{Die Konzeption des Scala-Layers}
neuper@42046: \begin{figure}
neuper@42046: \begin{center}
neuper@42046: \includegraphics[width=100mm]{fig-reuse-ml-scala-SD}
neuper@42046: \end{center}
neuper@42046: %\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.}
neuper@42046: \label{fig-reuse-ml-scala}
neuper@42046: \end{figure}
neuper@42042: \end{frame}
neuper@41965: 
neuper@42042: \begin{frame}\frametitle{Kommunikationsprotokoll \\Scala --- SML}
neuper@42042: \begin{itemize}
neuper@42042: \item Das Protokoll ist \textbf{asynchron}: \\
neuper@42042: verschiedene Teile eines Beweises werden in verschiedenen Threads interpretiert
neuper@42042: \pause
neuper@42042: \item Die Threads werden von Scala-\textbf{``Actors''} verwaltet (``Actors'' von der Programmsprache Erlang \"ubernommen)
neuper@42042: \pause
neuper@42042: \item \alert{Das Protokoll hat \textbf{kein API} nach aussen:}\\
neuper@42042: \pause
neuper@42042: Der Scala-Layer zielt auf konsistente Verwaltung gro\3er, verteilter Theorie-Bibliotheken\\
neuper@42042: \pause
neuper@42042: Anwendungsprogrammierer sollen nicht hier eingreifen, sondern Isabelle Theorien erweitern\\
neuper@42042: \pause
neuper@42042: \alert{\textit{!~Grunds\"atzliches Problem f\"ur das Projekt ``SD''~!}}
neuper@42042: \end{itemize}
neuper@42042: \end{frame}
neuper@41965: 
neuper@42042: \subsection[Integration]{Isabelles Filestruktur im \"Ubergangsstadium}
neuper@41965: 
m@42053: 
neuper@42046: \begin{frame}\frametitle{Isabelle Files: *.scala}
neuper@42046: {\tiny
neuper@42048: \textbf{\$ find -name ``*.scala''}\\
neuper@42046: ./src/Pure/General/xml.scala\\
neuper@42046: ./src/Pure/General/linear\_set.scala\\
m@42054: 
m@42054: ./src/Pure/General/symbol.scala\\
m@42054: ./src/Pure/General/exn.scala\\
m@42054: ./src/Pure/General/position.scala\\
m@42054: ./src/Pure/General/scan.scala\\
m@42054: ./src/Pure/General/xml\_data.scala\\
m@42054: ./src/Pure/General/yxml.scala\\
m@42054: ./src/Pure/General/markup.scala\\
neuper@42048: :\\
m@42054: ./src/Pure/General/sha1.scala\\
neuper@42046: ./src/Pure/General/timing.scala\\
neuper@42046: ./src/Pure/General/pretty.scala\\
neuper@42046: .\\
neuper@42046: ./src/Pure/Concurrent/volatile.scala\\
neuper@42046: ./src/Pure/Concurrent/future.scala\\
neuper@42046: ./src/Pure/Concurrent/simple\_thread.scala\\
neuper@42046: .\\
neuper@42046: ./src/Pure/Thy/html.scala\\
neuper@42046: ./src/Pure/Thy/completion.scala\\
neuper@42046: ./src/Pure/Thy/thy\_header.scala\\
neuper@42046: ./src/Pure/Thy/thy\_syntax.scala\\
neuper@42046: ./src/Pure/Isac/isac.scala\\
neuper@42046: ./src/Pure/library.scala\\
neuper@42046: .\\
neuper@42046: ./src/Pure/Isar/keyword.scala\\
neuper@42046: ./src/Pure/Isar/outer\_syntax.scala\\
neuper@42046: ./src/Pure/Isar/token.scala\\
neuper@42046: ./src/Pure/Isar/parse.scala\\
neuper@42046: .\\
neuper@42046: ./src/Pure/System/gui\_setup.scala\\
neuper@42046: ./src/Pure/System/isabelle\_system.scala\\
m@42054: ./src/Pure/General/timing.scala\\
m@42054: ./src/Pure/General/pretty.scala\\
m@42054: .\\
m@42054: ./src/Pure/Concurrent/volatile.scala\\
m@42054: ./src/Pure/Concurrent/future.scala\\
m@42054: ./src/Pure/Concurrent/simple\_thread.scala\\
m@42054: .\\
m@42054: ./src/Pure/Thy/html.scala\\
m@42054: ./src/Pure/Thy/completion.scala\\
m@42054: ./src/Pure/Thy/thy\_header.scala\\
m@42054: ./src/Pure/Thy/thy\_syntax.scala\\
m@42054: ./src/Pure/Isac/isac.scala\\
m@42054: ./src/Pure/library.scala\\
m@42054: .\\
m@42054: ./src/Pure/Isar/keyword.scala\\
m@42054: ./src/Pure/Isar/outer\_syntax.scala\\
m@42054: ./src/Pure/Isar/token.scala\\
m@42054: ./src/Pure/Isar/parse.scala\\
m@42054: .\\
m@42054: ./src/Pure/System/gui\_setup.scala\\
m@42054: ./src/Pure/System/isabelle\_system.scala\\
m@42054: ./src/Pure/System/swing\_thread.scala\\
m@42054: ./src/Pure/System/download.scala\\
m@42054: ./src/Pure/System/session\_manager.scala\\
m@42054: ./src/Pure/System/standard\_system.scala\\
m@42054: ./src/Pure/System/isabelle\_syntax.scala\\
m@42054: ./src/Pure/System/session.scala\\
m@42054: ./src/Pure/System/platform.scala\\
m@42054: ./src/Pure/System/cygwin.scala\\
neuper@42046: ./src/Pure/System/event\_bus.scala\\
neuper@42046: ./src/Pure/System/isabelle\_process.scala\\
neuper@42046: .\\
neuper@42046: ./src/Pure/PIDE/document.scala\\
neuper@42046: ./src/Pure/PIDE/markup\_tree.scala\\
neuper@42046: ./src/Pure/PIDE/text.scala\\
neuper@42046: ./src/Pure/PIDE/command.scala\\
neuper@42046: ./src/Pure/PIDE/isar\_document.scala
neuper@42046: }
neuper@42046: \end{frame}
neuper@42042: 
neuper@42042: 
neuper@42042: 
neuper@42042: \subsection[jEdit]{Das Frontend: jEdit und ``plugins''}
neuper@42042: \begin{frame}\frametitle{Das Frontend: \\jEdit und ``plugins''}
neuper@42042: \begin{itemize}
neuper@42042: \item \textbf{jEdit} \textit{``is a mature programmer's text editor with hundreds (counting the time developing \textbf{plugins}) of person-years of development behind it.''}
neuper@42042: \pause
neuper@42042: \item Also: Die Funktionalit\"at von jEdit wird \"uber ``plugins'' bestimmt
neuper@42042: \pause
neuper@42042: \item Isabelle verwendet eine Reihe davon
neuper@42042:   \begin{itemize}
neuper@42042:   \item der Parser ``Sidekick''
neuper@42042:   \item Console f\"ur jEdit-Komponenten
neuper@42042:   \item + Scala
neuper@42042:   \item + Ml
neuper@42042:   \item etc
neuper@42042:   \end{itemize}
neuper@42042: \pause
neuper@42042: \item jEdit ist ``open source'' mit gro\3er Community
neuper@42042: \pause
neuper@42042: \item Anfragen an Mailinglisten von jEdit (ohne Scala-plugin!) und Isabelle
neuper@42042: \end{itemize}
neuper@42042: \end{frame}
neuper@42042: 
neuper@42046: \section[Projektarbeit]{Projekt: Vorarbeiten f\"ur ``structured derivations'' (SD)}
neuper@42046: \subsection[Aufgabenstellung]{Definition der Aufgabenstellung}
neuper@42046: \begin{frame}\frametitle{Definition der Aufgabenstellung}
neuper@42048: Aufgabenstellung: \\Feasibility-Study zur Implementierung von ``structured~derivations'' (SD) in Isabelle.\\
neuper@42046: 
neuper@42046: \textit{``Die Implementierung soweit vorantreiben wie im gegebenen Studenausma\3 m\"oglich~!''}\\
neuper@42046: 
neuper@42046: Milestones:
neuper@42046: \begin{enumerate}
neuper@42046: \item Relevante Isabelle Komponenten identifizieren und studieren
neuper@42046: \item Installation der Standard-Komponenten
neuper@42046: \item Entwicklungsumgebung vom Isabelle-Team kopieren
neuper@42046: \item Relevante Komponenten implementieren
neuper@42046:   \begin{itemize}
neuper@42046:   \item jEdit Plugin f\"ur SD
neuper@42046:   \item zugeh\"origen Parser
neuper@42046:   \item nicht vorgesehen: SD-Interpreter in Isar (SML)
neuper@42046:   \end{itemize}
neuper@42046: \end{enumerate}
neuper@42046: \end{frame}
neuper@42046: 
neuper@42046: %\subsection[Beispiel SD]{Beispiel ``structured derivation'' (SD)}
neuper@42042: \begin{frame}\frametitle{Beispiel ``structured~derivation''~(SD)}
neuper@42042: {\footnotesize
neuper@42042: \begin{tabbing}
neuper@42042: 123,\=1234\=1234\=1234\=1234\=1234\=1234\=123\=\kill
neuper@42042: \>$\bullet$\>Simplify $(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
neuper@42042: \>  \>$(1 - x) * (x ^ 2 + 1) + x ^ 3 - x ^ 2$\\
neuper@42042: \>$\equiv$\>$\{ {\it RewriteSet}\;{\it purify}\}$\\
neuper@42042: \>  \>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
neuper@42042: \>$\equiv$\>$\{{\it RewriteSet}\;{\it simplify\_pure}\}$\\
neuper@42042: \>  \>$\bullet$\>$(1 + -1 * x) * (x ^ 2 + 1) + x ^ 3 + -1 * x ^ 2$\\
neuper@42042: \>  \>$\equiv$\>$\{{\it RewriteSet}\;{\it expand\_poly\_}\}$ \\
neuper@42042: \>  \>   \>$1 * x ^ 2 + 1 * 1 + (-1 * x * x ^ 2 + -1 * x * 1) + x ^ 3 +-1 * x ^ 2$\\
neuper@42042: \>  \>$\equiv$\>\vdots\\
neuper@42042: \>  \>  \>$1 + -1 * x + 0 * x ^ 2 + 0 * x ^ 3$\\
neuper@42042: \>  \>$\equiv$\>$\{{\it RewriteSet}\;{\it reduce\_012\_}\}$  \\
neuper@42042: \>  \>     \>$1 + -1 * x$\\
neuper@42042: \>\dots\>$1 + -1 * x$\\
neuper@42042: \>$\equiv$\>$\{{\it RewriteSet}\;{\it beautify}\}$\\
neuper@42042: \>  \>$1-x$
neuper@42042: \end{tabbing}
neuper@42042: }
neuper@42042: \end{frame}
neuper@42042: 
neuper@42046: \subsection[NetBeans]{Konfiguration des Projektes in der NetBeans IDE}
neuper@42046: \begin{frame}\frametitle{Konfiguration in NetBeans}
neuper@42046: Mehrere Run-Konfigurationen sind praktisch:
m@42043: \begin{itemize}
neuper@42046: \item Start von jEdit + Plug-ins aus NetBeans
neuper@42046:   \begin{itemize}
neuper@42046:   \item Exekution der fertig kompilierten jEdit.jar
neuper@42046:   \item Exkution der eingebundenen jEdit Sources: \\zum Debuggen !
neuper@42046:   \end{itemize}
neuper@42046: \item Start von jEdit aus der Konsole
neuper@42046: \end{itemize}
neuper@42046: \vspace{0.2cm}   \pause
neuper@42046: Dementsprechend komplex sind die Konfigurations-Files:
neuper@42046: \begin{center}
neuper@42046: \begin{tabular}{l r l}
neuper@42046: build.xml          & 102 & LOCs\\
neuper@42046: project.xml        & 25  & LOCs\\
neuper@42046: project.properties & 85  & LOCs\\
neuper@42046: build-impl.xml     & 708 & LOCs\\
neuper@42046:                    &     & (teilw. automatisch generiert)\end{tabular}
neuper@42046: \end{center}
neuper@42046: \end{frame}
neuper@42046: 
neuper@42046: \subsection[Implementation]{Komponenten zur Implementation von SD}
neuper@42046: 
neuper@42046: \begin{frame}\frametitle{Die Konzeption des Scala-Layers}
neuper@42046: \begin{figure}
neuper@42046: \includegraphics[width=100mm]{fig-jedit-plugins-SD}
neuper@42046: \label{Frontend des jEdit}
neuper@42046: \end{figure}
neuper@42046: \end{frame}
neuper@42046: 
neuper@42046: \begin{frame}\frametitle{jEdit-Plugin}
neuper@42046: \begin{itemize}
neuper@42046: \item Aufbau: Ein Plugin besteht aus:
m@42043: \pause
m@42043: 	\begin{itemize}
m@42043: 	\item Source-Files: \textbf{Scala} 
m@42043: 	\pause
m@42043: 	\item Property file 
m@42043: 	\pause
neuper@42046: 	\item XML-Files: \textit{``glue code''} zwischen \textbf{Java} (Editor) und \textbf{Scala} (Plugin)
m@42043: 	\end{itemize}
neuper@42046: %\pause
neuper@42046: %\item Bestehendes Java-Plugin in Scala transferieren
neuper@42046: %\pause
neuper@42046: %\item Neue Ordnerstruktur in bestehende Isabelle-Ordner-Hierachie integrieren
m@42043: \end{itemize}
m@42043: \end{frame}
m@42043: 
neuper@42048: \begin{frame}\frametitle{Sources des jEdit Plugins}
neuper@42048: {\tiny
neuper@42048: src/Tools/jEditC\textbf{\$ ls -l *}\\
neuper@42048: build.xml\\
neuper@42048: %makedist\\
neuper@42048: %manifest.mf\\
neuper@42048: %README\_BUILD\\
neuper@42048: \textbf{build/*}\\
neuper@42048: \textbf{contrib/*}\\
neuper@42048: \textbf{dist/*}\\
neuper@42048: \textbf{plugin/}build.xml\\
neuper@42048: \textbf{plugin/}changes40.txt\\
neuper@42048: \textbf{plugin/}changes42.txt\\
neuper@42048: \textbf{plugin/}description.html\\
neuper@42048: \textbf{plugin/}IsacActions.java\\
neuper@42048: \textbf{plugin/}Isac.iml\\
neuper@42048: \textbf{plugin/}Isac.java\\
neuper@42048: \textbf{plugin/}IsacOptionPane.java\\
neuper@42048: \textbf{plugin/}IsacPlugin.java\\
neuper@42048: \textbf{plugin/}IsacTextArea.java\\
neuper@42048: \textbf{plugin/}IsacToolPanel.java\\
neuper@42048: \textbf{plugin/}plugin\\
neuper@42048: \textbf{plugin/}README.txt\\
neuper@42048: \textbf{nbproject/*}\\
neuper@42048: \textbf{src/}actions.xml\\
neuper@42048: \textbf{src/}changes40.txt\\
neuper@42048: \textbf{src/}changes42.txt\\
neuper@42048: \textbf{src/}description.html\\
neuper@42048: \textbf{src/}dockables.xml\\
neuper@42048: \textbf{src/}IsacActions.scala\\
neuper@42048: \textbf{src/}Isac.iml\\
neuper@42048: \textbf{src/}IsacOptionPane.scala\\
neuper@42048: \textbf{src/}IsacPlugin.scala\\
neuper@42048: \textbf{src/}Isac.props\\
neuper@42048: \textbf{src/}Isac.scala\\
neuper@42048: \textbf{src/}IsacTextArea.scala\\
neuper@42048: \textbf{src/}IsacToolPanel.scala\\
neuper@42048: \textbf{src/}manifest.mf\\
neuper@42048: \textbf{src/}README.txt\\
neuper@42048: \textbf{src/}users-guide.xml
neuper@42048: }
neuper@42048: \end{frame}
neuper@42048: 
m@42043: \begin{frame}\frametitle{Anforderungen an das Versuchs-Plugin}
m@42043: Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt:
m@42043: \pause
m@42043: \begin{itemize}
m@42043: 	\item Grunds\"atzlicher Aufbau eines GUIs
m@42043: 	\pause
neuper@42046: 	\item Kopieren von Text zwischen den einzelnen Buffers
m@42043: 	\pause
m@42043: 		\begin{itemize}
m@42043: 		\item \alert{Somit auch Zugriff auf andere Plugins!}
m@42043: 		\end{itemize}
m@42043: 	\pause
m@42043: 	\item Ansatz f\"ur die Einbindung des SD-Parsers
m@42043: 	\pause
m@42043: 		\begin{itemize}
m@42043: 		\item Zugriff auf Isabelle-Pure: \alert{parsen von SD parallel zu Isabelle/Isar}
m@42043: 		\end{itemize}
m@42043: 	\pause
m@42043: 	\item \textit{DEMO}
m@42043: \end{itemize}
m@42043: \end{frame}
m@42043: 
neuper@42046: 
neuper@42048: %\subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)}
neuper@42042: 
neuper@42042: \section[Summary]{Zusammenfassung}
neuper@42042: \begin{frame}\frametitle{Zusammenfassung}
neuper@42046: Folgende Milestones wurden erfolgreich abgeschlossen:
neuper@42046: \begin{enumerate}
m@42049: \item Relevante Isabelle Komponenten dokumentiert
m@42049: \pause
neuper@42046: \item Installation der Standard-Komponenten:
neuper@42046:   \begin{itemize}
neuper@42046:   \item Mercurial Versioncontrol
neuper@42046:   \item NetBeans IDE
neuper@42046:   \item Standard Isabelle Bundle
neuper@42046:   \end{itemize}
m@42049:   \pause
neuper@42046: \item Entwicklungsumgebung vom Isabelle-Team kopieren
neuper@42046:   \begin{itemize}
neuper@42046:   \item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML)
neuper@42046:   \item jEdit als NetBeans Projekt definiert
neuper@42046:   \end{itemize}
m@42049:   \pause
neuper@42046: \item Relevante Komponenten implementieren
neuper@42046:   \begin{itemize}
neuper@42046:   \item jEdit Plugin f\"ur SD
neuper@42046:   \item Verbindung des Plugins zu Isabelle
neuper@42046:   \item zugeh\"origen Parser: nur ein Test in SML
neuper@42046:   \end{itemize}
neuper@42046: \end{enumerate}
neuper@42046: \end{frame}
neuper@42046: 
neuper@42046: \begin{frame}\frametitle{Zusammenfassung}
neuper@42046: \pause
neuper@42046: \alert{$\mathbf{- - -}$}\\
neuper@42046: Aus Zeitgr\"unden nicht m\"oglich: ein komplettes SD-Plugin;\\
neuper@42046: dazu w\"are auch ein Interpreter auf der ML-Seite n\"otig.\\
neuper@42046: \vspace{0.3cm}
neuper@42046: \alert{$\mathbf{+ + +}$}\\
m@42049: \pause
neuper@42046: Voraussetzungen f\"ur k\"unftige Entwicklung geschaffen:
neuper@42046: \begin{enumerate}
neuper@42046: \item f\"ur die Implementation von ``structured derivations'' in Isabelle \dots
neuper@42046: \item \dots als Vorarbeit f\"ur jEdit als k\"unftiges \isac-Frontend
neuper@42046: \item f\"ur Mitarbeit an k\"unftiger Integration von Isabelle in Entwicklungswerkzeuge (Testcase-Generation etc).
neuper@42046: \end{enumerate}
neuper@42042: \end{frame}
neuper@42042: 
neuper@42042: \begin{frame}\frametitle{}
neuper@42046: \begin{center}
neuper@42046: \LARGE{Danke f\"ur die Aufmerksamkeit !}
neuper@42046: \end{center}
neuper@41965: \end{frame}
neuper@41965: 
neuper@41965: \end{document}
neuper@41965: 
neuper@41965: 




