neuper@41965: % /usr/share/doc/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex neuper@41965: neuper@41965: \documentclass{beamer} neuper@41965: \mode 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: neuper@41965: \date{TODO} 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} 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} neuper@42042: \item Demo $\sqrt{2}\not\in{\cal R}\;\;\;$ 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: neuper@42042: \begin{frame}\frametitle{Isabelle Files: *.scala} neuper@42042: {\tiny neuper@42048: \textbf{\$ find -name ``*.scala''}\\ neuper@42042: ./src/Pure/General/xml.scala\\ neuper@42042: ./src/Pure/General/linear\_set.scala\\ neuper@42048: %./src/Pure/General/symbol.scala\\ neuper@42048: %./src/Pure/General/exn.scala\\ neuper@42048: %./src/Pure/General/position.scala\\ neuper@42048: %./src/Pure/General/scan.scala\\ neuper@42048: %./src/Pure/General/xml\_data.scala\\ neuper@42048: %./src/Pure/General/yxml.scala\\ neuper@42048: %./src/Pure/General/markup.scala\\ neuper@42048: :\\ neuper@42048: %./src/Pure/General/sha1.scala\\ neuper@42042: ./src/Pure/General/timing.scala\\ neuper@42042: ./src/Pure/General/pretty.scala\\ neuper@42042: .\\ neuper@42042: ./src/Pure/Concurrent/volatile.scala\\ neuper@42042: ./src/Pure/Concurrent/future.scala\\ neuper@42042: ./src/Pure/Concurrent/simple\_thread.scala\\ neuper@42042: .\\ neuper@42042: ./src/Pure/Thy/html.scala\\ neuper@42042: ./src/Pure/Thy/completion.scala\\ neuper@42042: ./src/Pure/Thy/thy\_header.scala\\ neuper@42042: ./src/Pure/Thy/thy\_syntax.scala\\ neuper@42042: ./src/Pure/Isac/isac.scala\\ neuper@42042: ./src/Pure/library.scala\\ neuper@42042: .\\ neuper@42042: ./src/Pure/Isar/keyword.scala\\ neuper@42042: ./src/Pure/Isar/outer\_syntax.scala\\ neuper@42042: ./src/Pure/Isar/token.scala\\ neuper@42042: ./src/Pure/Isar/parse.scala\\ neuper@42042: .\\ neuper@42042: ./src/Pure/System/gui\_setup.scala\\ neuper@42042: ./src/Pure/System/isabelle\_system.scala\\ neuper@42048: %./src/Pure/System/swing\_thread.scala\\ neuper@42048: %./src/Pure/System/download.scala\\ neuper@42048: %./src/Pure/System/session\_manager.scala\\ neuper@42048: %./src/Pure/System/standard\_system.scala\\ neuper@42048: %./src/Pure/System/isabelle\_syntax.scala\\ neuper@42048: %./src/Pure/System/session.scala\\ neuper@42048: %./src/Pure/System/platform.scala\\ neuper@42048: %./src/Pure/System/cygwin.scala\\ neuper@42048: :\\ neuper@42042: ./src/Pure/System/event\_bus.scala\\ neuper@42042: ./src/Pure/System/isabelle\_process.scala\\ neuper@42042: .\\ neuper@42042: ./src/Pure/PIDE/document.scala\\ neuper@42042: ./src/Pure/PIDE/markup\_tree.scala\\ neuper@42042: ./src/Pure/PIDE/text.scala\\ neuper@42042: ./src/Pure/PIDE/command.scala\\ neuper@42042: ./src/Pure/PIDE/isar\_document.scala neuper@42042: } neuper@42042: \end{frame} neuper@42042: neuper@42042: \begin{frame}\frametitle{*.scala --- *.ML} neuper@42042: {\footnotesize neuper@42042: isabisac\$ ls -l src/Pure/System/\\ neuper@42042: -rw-r--r-- 1 msteger root 3987 2011-03-14 17:09 cygwin.scala\\ neuper@42042: -rw-r--r-- 1 msteger root 1486 2011-03-14 17:09 download.scala\\ neuper@42042: -rw-r--r-- 1 msteger root 1296 2011-03-14 17:09 event\_bus.scala\\ neuper@42042: -rw-r--r-- 1 msteger root 1830 2011-03-14 17:09 gui\_setup.scala\\ neuper@42042: -rw-r--r-- 1 msteger root 5722 2011-03-14 17:09 \alert{isabelle\_process}.\textbf{ML}\\ neuper@42042: -rw-r--r-- 1 msteger root 1059 2011-03-14 17:09 \alert{isabelle\_process}.\textbf{scala}\\ neuper@42042: -rw-r--r-- 1 msteger root 1659 2011-03-14 17:09 isabelle\_syntax.scala\\ neuper@42042: -rw-r--r-- 1 msteger root 2087 2011-03-14 17:09 \alert{isabelle\_system}.\textbf{ML}\\ neuper@42042: -rw-r--r-- 1 msteger root 1168 2011-03-14 17:09 \alert{isabelle\_system}.\textbf{scala}\\ neuper@42042: -rw-r--r-- 1 msteger root 5935 2011-03-14 17:09 isar.ML\\ neuper@42042: -rw-r--r-- 1 msteger root 1989 2011-03-14 17:09 platform.scala\\ neuper@42042: -rw-r--r-- 1 msteger root 1427 2011-03-14 17:09 session\_manager.scala\\ neuper@42042: -rw-r--r-- 1 msteger root 3833 2011-03-14 17:09 \alert{session}.\textbf{ML}\\ neuper@42042: -rw-r--r-- 1 msteger root 9172 2011-03-14 17:09 \alert{session}.\textbf{scala}\\ neuper@42042: -rw-r--r-- 1 msteger root 9086 2011-03-14 17:09 standard\_system.scala\\ neuper@42042: -rw-r--r-- 1 msteger root 1643 2011-03-14 17:09 swing\_thread.scala\\ neuper@42042: neuper@42042: } neuper@42042: \end{frame} 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} neuper@42046: \item Relevante Isabelle Komponenten dokumentiert (...Std.) 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} 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} 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{+ + +}$}\\ 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: