1.1 --- a/doc-src/isac/msteger/bakk-presentation.tex Mon Jun 20 17:33:06 2011 +0200
1.2 +++ b/doc-src/isac/msteger/bakk-presentation.tex Wed Jun 22 19:48:14 2011 +0200
1.3 @@ -26,7 +26,7 @@
1.4 \institute{Institut f\"ur Software Technologie\\
1.5 Technische Universit\"at Graz}
1.6
1.7 -\date{TODO}
1.8 +\date{21.06.2011}
1.9 %\subject{Formal specification of math assistants}
1.10 % This is only inserted into the PDF information catalog
1.11
1.12 @@ -88,7 +88,8 @@
1.13 \pause
1.14 \item Isar, die Beweissprache von Isabelle
1.15 \begin{itemize}
1.16 - \item Demo $\sqrt{2}\not\in{\cal R}\;\;\;$
1.17 + %\item Demo $\sqrt{2}\not\in{\cal R}\;\;\;$
1.18 + \item Demo 'Allgemeine Dreiecke'
1.19 \pause
1.20 \alert{Beweisteile asynchron interpretiert}
1.21 \end{itemize}
1.22 @@ -124,12 +125,62 @@
1.23 \end{frame}
1.24
1.25 \subsection[Integration]{Isabelles Filestruktur im \"Ubergangsstadium}
1.26 +<<<<<<< local
1.27
1.28 +=======
1.29 +>>>>>>> other
1.30 +
1.31 +<<<<<<< local
1.32 +%\begin{frame}\frametitle{Isabelle Files: *.jar}
1.33 +%{\footnotesize
1.34 +%----- for ``isabelle jedit \&''; contained in Isabelle\_bundle}\\
1.35 +%{\tiny
1.36 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jedit.jar\\
1.37 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/LatestVersion.jar\\
1.38 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/SideKick.jar\\
1.39 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Console.jar\\
1.40 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Pure.jar \alert{$\;\;\;\;\;\;\;\;\;\;\;\Longleftarrow$ entry to SML}\\
1.41 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isac.jar\\
1.42 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-compiler.jar\\
1.43 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isabelle-jEdit.jar\\
1.44 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/cobra.jar\\
1.45 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/js.jar\\
1.46 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Hyperlinks.jar\\
1.47 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-swing.jar\\
1.48 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-library.jar\\
1.49 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/QuickNotepad.jar\\
1.50 +%./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/ErrorList.jar\\
1.51 +%
1.52 +%{\footnotesize
1.53 +%----- scala system; contained in Isabelle\_bundle}\\
1.54 +%./contrib/scala-2.8.1.final/misc/sbaz/scala-bazaars.jar\\
1.55 +%./contrib/scala-2.8.1.final/misc/sbaz/sbaz-tests.jar\\
1.56 +%./contrib/scala-2.8.1.final/misc/scala-devel/plugins/continuations.jar\\
1.57 +%./contrib/scala-2.8.1.final/lib/scala-compiler.jar\\
1.58 +%./contrib/scala-2.8.1.final/lib/scalap.jar\\
1.59 +%./contrib/scala-2.8.1.final/lib/scala-swing.jar\\
1.60 +%./contrib/scala-2.8.1.final/lib/scala-library.jar\\
1.61 +%./contrib/scala-2.8.1.final/lib/jline.jar\\
1.62 +%./contrib/scala-2.8.1.final/lib/scala-dbc.jar\\
1.63 +%./contrib/scala-2.8.1.final/src/scala-library-src.jar\\
1.64 +%./contrib/scala-2.8.1.final/src/scala-swing-src.jar\\
1.65 +%./contrib/scala-2.8.1.final/src/scala-compiler-src.jar\\
1.66 +%./contrib/scala-2.8.1.final/src/scala-dbc-src.jar\\
1.67 +%./contrib/scala-2.8.1.final/src/sbaz-src.jar\\
1.68 +%}
1.69 +%\end{frame}
1.70 +%
1.71 +%\begin{frame}\frametitle{Isabelle Files: *.scala}
1.72 +%{\tiny
1.73 +%./src/Pure/General/xml.scala\\
1.74 +%./src/Pure/General/linear\_set.scala\\
1.75 +=======
1.76 \begin{frame}\frametitle{Isabelle Files: *.scala}
1.77 {\tiny
1.78 \textbf{\$ find -name ``*.scala''}\\
1.79 ./src/Pure/General/xml.scala\\
1.80 ./src/Pure/General/linear\_set.scala\\
1.81 +>>>>>>> other
1.82 %./src/Pure/General/symbol.scala\\
1.83 %./src/Pure/General/exn.scala\\
1.84 %./src/Pure/General/position.scala\\
1.85 @@ -137,8 +188,34 @@
1.86 %./src/Pure/General/xml\_data.scala\\
1.87 %./src/Pure/General/yxml.scala\\
1.88 %./src/Pure/General/markup.scala\\
1.89 +<<<<<<< local
1.90 +=======
1.91 :\\
1.92 +>>>>>>> other
1.93 %./src/Pure/General/sha1.scala\\
1.94 +<<<<<<< local
1.95 +%./src/Pure/General/timing.scala\\
1.96 +%./src/Pure/General/pretty.scala\\
1.97 +%.\\
1.98 +%./src/Pure/Concurrent/volatile.scala\\
1.99 +%./src/Pure/Concurrent/future.scala\\
1.100 +%./src/Pure/Concurrent/simple\_thread.scala\\
1.101 +%.\\
1.102 +%./src/Pure/Thy/html.scala\\
1.103 +%./src/Pure/Thy/completion.scala\\
1.104 +%./src/Pure/Thy/thy\_header.scala\\
1.105 +%./src/Pure/Thy/thy\_syntax.scala\\
1.106 +%./src/Pure/Isac/isac.scala\\
1.107 +%./src/Pure/library.scala\\
1.108 +%.\\
1.109 +%./src/Pure/Isar/keyword.scala\\
1.110 +%./src/Pure/Isar/outer\_syntax.scala\\
1.111 +%./src/Pure/Isar/token.scala\\
1.112 +%./src/Pure/Isar/parse.scala\\
1.113 +%.\\
1.114 +%./src/Pure/System/gui\_setup.scala\\
1.115 +%./src/Pure/System/isabelle\_system.scala\\
1.116 +=======
1.117 ./src/Pure/General/timing.scala\\
1.118 ./src/Pure/General/pretty.scala\\
1.119 .\\
1.120 @@ -160,6 +237,7 @@
1.121 .\\
1.122 ./src/Pure/System/gui\_setup.scala\\
1.123 ./src/Pure/System/isabelle\_system.scala\\
1.124 +>>>>>>> other
1.125 %./src/Pure/System/swing\_thread.scala\\
1.126 %./src/Pure/System/download.scala\\
1.127 %./src/Pure/System/session\_manager.scala\\
1.128 @@ -168,6 +246,18 @@
1.129 %./src/Pure/System/session.scala\\
1.130 %./src/Pure/System/platform.scala\\
1.131 %./src/Pure/System/cygwin.scala\\
1.132 +<<<<<<< local
1.133 +%./src/Pure/System/event\_bus.scala\\
1.134 +%./src/Pure/System/isabelle\_process.scala\\
1.135 +%.\\
1.136 +%./src/Pure/PIDE/document.scala\\
1.137 +%./src/Pure/PIDE/markup\_tree.scala\\
1.138 +%./src/Pure/PIDE/text.scala\\
1.139 +%./src/Pure/PIDE/command.scala\\
1.140 +%./src/Pure/PIDE/isar\_document.scala
1.141 +%}
1.142 +%\end{frame}
1.143 +=======
1.144 :\\
1.145 ./src/Pure/System/event\_bus.scala\\
1.146 ./src/Pure/System/isabelle\_process.scala\\
1.147 @@ -179,6 +269,7 @@
1.148 ./src/Pure/PIDE/isar\_document.scala
1.149 }
1.150 \end{frame}
1.151 +>>>>>>> other
1.152
1.153 \begin{frame}\frametitle{*.scala --- *.ML}
1.154 {\footnotesize
1.155 @@ -392,18 +483,21 @@
1.156 \begin{frame}\frametitle{Zusammenfassung}
1.157 Folgende Milestones wurden erfolgreich abgeschlossen:
1.158 \begin{enumerate}
1.159 -\item Relevante Isabelle Komponenten dokumentiert (...Std.)
1.160 +\item Relevante Isabelle Komponenten dokumentiert
1.161 +\pause
1.162 \item Installation der Standard-Komponenten:
1.163 \begin{itemize}
1.164 \item Mercurial Versioncontrol
1.165 \item NetBeans IDE
1.166 \item Standard Isabelle Bundle
1.167 \end{itemize}
1.168 + \pause
1.169 \item Entwicklungsumgebung vom Isabelle-Team kopieren
1.170 \begin{itemize}
1.171 \item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML)
1.172 \item jEdit als NetBeans Projekt definiert
1.173 \end{itemize}
1.174 + \pause
1.175 \item Relevante Komponenten implementieren
1.176 \begin{itemize}
1.177 \item jEdit Plugin f\"ur SD
1.178 @@ -420,6 +514,7 @@
1.179 dazu w\"are auch ein Interpreter auf der ML-Seite n\"otig.\\
1.180 \vspace{0.3cm}
1.181 \alert{$\mathbf{+ + +}$}\\
1.182 +\pause
1.183 Voraussetzungen f\"ur k\"unftige Entwicklung geschaffen:
1.184 \begin{enumerate}
1.185 \item f\"ur die Implementation von ``structured derivations'' in Isabelle \dots
2.1 Binary file doc-src/isac/msteger/fig-jedit-plugins-SD.odg has changed
3.1 Binary file doc-src/isac/msteger/fig-reuse-ml-scala-SD.odg has changed