1 % $Header: /cvsroot/latex-beamer/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex,v 1.7 2007/01/28 20:48:23 tantau Exp $ |
|
2 |
|
3 \documentclass{beamer} |
|
4 |
|
5 % This file is a solution template for: |
|
6 |
|
7 % - Talk at a conference/colloquium. |
|
8 % - Talk length is about 20min. |
|
9 % - Style is ornate. |
|
10 |
|
11 |
|
12 |
|
13 % Copyright 2004 by Till Tantau <tantau@users.sourceforge.net>. |
|
14 % |
|
15 % In principle, this file can be redistributed and/or modified under |
|
16 % the terms of the GNU Public License, version 2. |
|
17 % |
|
18 % However, this file is supposed to be a template to be modified |
|
19 % for your own needs. For this reason, if you use this file as a |
|
20 % template and not specifically distribute it as part of a another |
|
21 % package/program, I grant the extra permission to freely copy and |
|
22 % modify this file as you see fit and even to delete this copyright |
|
23 % notice. |
|
24 |
|
25 |
|
26 \mode<presentation> |
|
27 { |
|
28 \usetheme{Hannover} |
|
29 % or ... |
|
30 |
|
31 \setbeamercovered{transparent} |
|
32 % or whatever (possibly just delete it) |
|
33 } |
|
34 |
|
35 %\usepackage{setspace} %for "\begin{onehalfspace}" |
|
36 \usepackage[english]{babel} |
|
37 % or whatever |
|
38 |
|
39 \usepackage[utf8]{inputenc} |
|
40 % or whatever |
|
41 |
|
42 \usepackage{times} |
|
43 \usepackage[T1]{fontenc} |
|
44 % Or whatever. Note that the encoding and the font should match. If T1 |
|
45 % does not look nice, try deleting the line with the fontenc. |
|
46 |
|
47 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
|
48 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} |
|
49 |
|
50 \title[\isac: Computation \& Deduction] % (optional, use only with long paper titles) |
|
51 {Integrating Computation and Deduction\\ |
|
52 in the \isac-System} |
|
53 |
|
54 \subtitle{Projektpraktikum: Introducing Isabelle's Contexts} |
|
55 |
|
56 \author[Lehnfeld] % (optional, use only with lots of authors) |
|
57 {Mathias~Lehnfeld} |
|
58 % - Give the names in the same order as the appear in the paper. |
|
59 % - Use the \inst{?} command only if the authors have different |
|
60 % affiliation. |
|
61 |
|
62 \institute % (optional, but mostly needed) |
|
63 { |
|
64 Vienna University of Technology\\ |
|
65 Institute of Computer Languages |
|
66 } |
|
67 % - Use the \inst command only if there are several affiliations. |
|
68 % - Keep it simple, no one is interested in your street address. |
|
69 |
|
70 % \date[CFP 2003] % (optional, should be abbreviation of conference name) |
|
71 % {Conference on Fabulous Presentations, 2003} |
|
72 % - Either use conference name or its abbreviation. |
|
73 % - Not really informative to the audience, more for people (including |
|
74 % yourself) who are reading the slides online |
|
75 |
|
76 % \subject{Theoretical Computer Science} |
|
77 % This is only inserted into the PDF information catalog. Can be left |
|
78 % out. |
|
79 |
|
80 |
|
81 |
|
82 % If you have a file called "university-logo-filename.xxx", where xxx |
|
83 % is a graphic format that can be processed by latex or pdflatex, |
|
84 % resp., then you can add a logo as follows: |
|
85 |
|
86 % \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename} |
|
87 % \logo{\pgfuseimage{university-logo}} |
|
88 |
|
89 |
|
90 |
|
91 % Delete this, if you do not want the table of contents to pop up at |
|
92 % the beginning of each subsection: |
|
93 \AtBeginSubsection[] |
|
94 { |
|
95 \begin{frame}<beamer>{Outline} |
|
96 \tableofcontents[currentsection,currentsubsection] |
|
97 \end{frame} |
|
98 } |
|
99 |
|
100 |
|
101 % If you wish to uncover everything in a step-wise fashion, uncomment |
|
102 % the following command: |
|
103 |
|
104 %\beamerdefaultoverlayspecification{<+->} |
|
105 |
|
106 |
|
107 \begin{document} |
|
108 |
|
109 \begin{frame} |
|
110 \titlepage |
|
111 \end{frame} |
|
112 |
|
113 \begin{frame}{Outline} |
|
114 \tableofcontents |
|
115 % You might wish to add the option [pausesections] |
|
116 \end{frame} |
|
117 |
|
118 |
|
119 % Structuring a talk is a difficult task and the following structure |
|
120 % may not be suitable. Here are some rules that apply for this |
|
121 % solution: |
|
122 |
|
123 % - Exactly two or three sections (other than the summary). |
|
124 % - At *most* three subsections per section. |
|
125 % - Talk about 30s to 2min per frame. So there should be between about |
|
126 % 15 and 30 frames, all told. |
|
127 |
|
128 % - A conference audience is likely to know very little of what you |
|
129 % are going to talk about. So *simplify*! |
|
130 % - In a 20min talk, getting the main ideas across is hard |
|
131 % enough. Leave out details, even if it means being less precise than |
|
132 % you think necessary. |
|
133 % - If you omit details that are vital to the proof/implementation, |
|
134 % just say so once. Everybody will be happy with that. |
|
135 |
|
136 \section[Introduction]{Introduction: Isabelle and \isac} |
|
137 %\subsection[Isabelle \& \isac]{Isabelle and \isac} |
|
138 \begin{frame} |
|
139 \frametitle{Isabelle and \isac} |
|
140 The task of this ``Projektpraktikum'' (6 ECTS) was to |
|
141 \begin{itemize} |
|
142 \item study the concept of ``context'' in the theorem prover \textbf{Isabelle} from TU Munich |
|
143 \item study basic concepts of the math assistant \sisac{} from TU Graz |
|
144 \pause |
|
145 \item redesign \sisac{} with respect to contexts |
|
146 \begin{itemize} |
|
147 \item use contexts for type inference of user input |
|
148 \item handle preconditions of specifications |
|
149 \item clarify the transfer of context data from sub-programs to the calling program |
|
150 \end{itemize} |
|
151 \pause |
|
152 \item introduce contexts to \sisac{} according to the new design |
|
153 \item use the coding standards of Isabelle2011 for new code. |
|
154 \end{itemize} |
|
155 \end{frame} |
|
156 |
|
157 %\subsection[Computation \& Deduction]{Computation and Deduction in a Lucas-Interpreter} |
|
158 \begin{frame} |
|
159 \frametitle{Computation and Deduction in a Lucas-Interpreter} |
|
160 \includegraphics[width=100mm]{overview.pdf} |
|
161 \end{frame} |
|
162 |
|
163 \section[Contributions]{Contributions of the project to \isac} |
|
164 \subsection[Contexts]{Isabelle's Contexts, advantages and use} |
|
165 \begin{frame} |
|
166 \frametitle{Advantages of Isabelle's Contexts} |
|
167 Isabelle's context replaced theories because \dots: |
|
168 \begin{itemize} |
|
169 \item theories are static containers of \textit{all} logical data |
|
170 \item contexts are \textit{dynamic} containers of logical data: |
|
171 \begin{itemize} |
|
172 \item functions for storing and retrieving various logical data |
|
173 \item functions for type inference |
|
174 \item provide data for Isabelle's automated provers |
|
175 \end{itemize} |
|
176 %\item e.g. theories have no direct functions for type inference |
|
177 %\item replace function \texttt{parseNEW} |
|
178 %\item assumptions \& environment $\rightarrow$ context |
|
179 \item allow to conform with scopes for subprograms. |
|
180 \end{itemize} |
|
181 \end{frame} |
|
182 |
|
183 \begin{frame} |
|
184 \frametitle{Isabelle's context mechanism} |
|
185 \texttt{\small{ |
|
186 \begin{tabbing} |
|
187 xx\=xx\=in\=\kill |
|
188 %xx\=xx\=xx\=xx\=\kill |
|
189 %datatype Isac\_Ctxt =\\ |
|
190 %\>\>Env of term * term\\ |
|
191 %\>| Asm of term;\\ |
|
192 %\\ |
|
193 structure ContextData = \alert{Proof\_Data}\\ |
|
194 \>~(\alert{type T} = term list\\ |
|
195 \>\>\alert{fun init \_} = []);\\ |
|
196 \\ |
|
197 %local\\ |
|
198 %\>fun insert\_ctxt data = ContextData\alert{.map} (fn xs => distinct (data@xs));\\ |
|
199 %in\\ |
|
200 %\>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\ |
|
201 %\>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\ |
|
202 %end\\ |
|
203 fun insert\_assumptions asms = \\ |
|
204 \>\>\>ContextData\alert{.map} (fn xs => distinct (asms@xs));\\ |
|
205 \\ |
|
206 %local\\ |
|
207 %\>fun unpack\_asms (Asm t::ts) = t::(unpack\_asms ts)\\ |
|
208 %\>\>| unpack\_asms (Env \_::ts) = unpack\_asms ts\\ |
|
209 %\>\>| unpack\_asms [] = [];\\ |
|
210 %\>fun unpack\_envs (Env t::ts) = t::(unpack\_envs ts)\\ |
|
211 %\>\>| unpack\_envs (Asm \_::ts) = unpack\_envs ts\\ |
|
212 %\>\>| unpack\_envs [] = [];\\ |
|
213 %in\\ |
|
214 %\>fun get\_assumptions ctxt = ContextData.get ctxt |> unpack\_asms;\\ |
|
215 %\>fun get\_environments ctxt = ContextData.get ctxt |> unpack\_envs;\\ |
|
216 %end |
|
217 fun get\_assumptions ctxt = ContextData\alert{.get} ctxt;\\ |
|
218 \\ |
|
219 \\ |
|
220 val declare\_constraints : \\ |
|
221 \>\>\>term -> Proof.context -> Proof.context |
|
222 \end{tabbing} |
|
223 }} |
|
224 \end{frame} |
|
225 |
|
226 \begin{frame} |
|
227 \frametitle{Usage of Contexts} |
|
228 \texttt{\footnotesize{ |
|
229 \begin{tabbing} |
|
230 xx\=xx\=xx\=xx\=xx\=\kill |
|
231 fun transfer\_asms\_from\_to from\_ctxt to\_ctxt =\\ |
|
232 \> let\\ |
|
233 \>\> val to\_vars = get\_assumptions to\_ctxt |> map vars |> flat\\ |
|
234 \>\> fun transfer [] to\_ctxt = to\_ctxt\\ |
|
235 \>\>\> | transfer (from\_asm::fas) to\_ctxt =\\ |
|
236 \>\>\>\>\> if inter op = (vars from\_asm) to\_vars = []\\ |
|
237 \>\>\>\>\> then transfer fas to\_ctxt\\ |
|
238 \>\>\>\>\> else transfer fas (insert\_assumptions [from\_asm] to\_ctxt)\\ |
|
239 \> in transfer (get\_assumptions from\_ctxt) to\_ctxt end\\ |
|
240 \\ |
|
241 fun parse thy str =\\ |
|
242 \>(let val t = (\alert{typ\_a2real} o numbers\_to\_string)\\ |
|
243 \>\>\>\>(\alert{Syntax.read\_term\_global thy} str)\\ |
|
244 \>\>in SOME (cterm\_of thy t) end)\\ |
|
245 \>\>\>handle \_ => NONE;\\ |
|
246 \\ |
|
247 fun parseNEW ctxt str = \\ |
|
248 \>\>\>SOME (\alert{Syntax.read\_term ctxt} str |> numbers\_to\_string)\\ |
|
249 \>\>\>handle \_ => NONE; |
|
250 \end{tabbing} |
|
251 }} |
|
252 |
|
253 |
|
254 \end{frame} |
|
255 |
|
256 \subsection[Redesign]{Redesign of \isac{} using contexts} |
|
257 \begin{frame} |
|
258 \frametitle{Redesign of \isac{} using contexts} |
|
259 \begin{center} DEMO \end{center} |
|
260 \end{frame} |
|
261 |
|
262 \begin{frame} |
|
263 \frametitle{Deduction simplifies computation} |
|
264 \small{ |
|
265 %\begin{onehalfspace} |
|
266 \begin{tabbing} |
|
267 xxx\=xxx\=\kill |
|
268 \`$\mathit{(some)}\;\mathit{assumptions}$\\ |
|
269 $\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\ |
|
270 % \`$x ^ 2 - 6 * x + 9\not=0\land x ^ 2 - 3 * x\not=0$\\ |
|
271 %\>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\ |
|
272 %\>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\ |
|
273 \>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\ |
|
274 \`$x\not=3\land x\not=0$\\ |
|
275 \>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\ |
|
276 \>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\ |
|
277 %\>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\ |
|
278 %\>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\ |
|
279 \>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\ |
|
280 \>\>$-6 * x + 5 * x ^ 2 = 0$ \\ |
|
281 \>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\ |
|
282 \>\>$[x = 0, x = \frac{6}{5}]$ \\ |
|
283 \`$x = 0\land x = \frac{6}{5}$\\ |
|
284 \>$[\alert{x = 0}, x = \frac{6}{5}]$ \\ |
|
285 \`\alert{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}:x\not=0\land x = 0$}\\ |
|
286 \>$[x = \frac{6}{5}]$ \\ |
|
287 $[x = \frac{6}{5}]$ |
|
288 \end{tabbing} |
|
289 } |
|
290 %\end{onehalfspace} |
|
291 \end{frame} |
|
292 |
|
293 \begin{frame} |
|
294 \frametitle{More ``deduction'', \\less ``computation''} |
|
295 \footnotesize{\tt |
|
296 \begin{tabbing} |
|
297 xx\=xx\=xx\=xx\=xx\=xx\=\kill |
|
298 Script Solve\_root\_equation (e\_e::bool) (v\_v::real) = \\ |
|
299 \> (let e\_e = ((Try (Rewrite\_Set norm\_equation False)) \@\@ \\ |
|
300 \>\>\> (Try (Rewrite\_Set Test\_simplify False))) e\_e; \\ |
|
301 \>\> (L\_L::bool list) = \\ |
|
302 \>\>\> (SubProblem (Test', \\ |
|
303 \>\>\>\> [linear,univariate,equation,test]\\ |
|
304 \>\>\>\> [Test,solve\_linear]) \\ |
|
305 \>\>\>\> [BOOL e\_e, REAL v\_v]) \\ |
|
306 \> in \alert{Check\_elementwise L\_L \{(v\_v::real). Assumptions\}})\\ |
|
307 \end{tabbing} |
|
308 } |
|
309 \small{ |
|
310 ``Deductive'' part of Lucas-Interpretation relives the ``computational'' part: \alert{one statement becomes obsolete~!} |
|
311 } |
|
312 \end{frame} |
|
313 |
|
314 |
|
315 \begin{frame} |
|
316 \frametitle{Redesign of \isac{} using contexts} |
|
317 Advantages of the redesign: |
|
318 \begin{itemize} |
|
319 \item type inference by \textit{local} contexts\\ |
|
320 \pause |
|
321 \alert{now user-input without type constraints~!} |
|
322 \pause |
|
323 \item consistent handling of logical data |
|
324 \begin{itemize} |
|
325 \item preconditions and partiality conditions in contexts |
|
326 \item transfer of context data into subprograms clarified |
|
327 \item transfer of context data from subprograms clarified |
|
328 \end{itemize} |
|
329 \pause |
|
330 \alert{now some statements become obsolete.}\\ |
|
331 \end{itemize} |
|
332 \pause |
|
333 Now Lucas-interpretation shifts efforts from ``computation'' further to ``deduction''. |
|
334 \end{frame} |
|
335 |
|
336 |
|
337 |
|
338 \subsection[Code Improvement]{Improvement of functional code} |
|
339 \begin{frame} |
|
340 \frametitle{Improvement of functional code} |
|
341 \begin{itemize} |
|
342 \item \textbf{code conventions}: Isabelle2011 published coding standards first time |
|
343 \item \textbf{combinators}: Isabelle2011 introduced a library containing the following combinators: |
|
344 \\\vspace{0.2cm} |
|
345 \tiny{\tt% |
|
346 val |$>$ : 'a * ('a -$>$ 'b) -$>$ 'b\\ |
|
347 val |-$>$ : ('c * 'a) * ('c -$>$ 'a -$>$ 'b) -$>$ 'b\\ |
|
348 val |$>>$ : ('a * 'c) * ('a -$>$ 'b) -$>$ 'b * 'c\\ |
|
349 val ||$>$ : ('c * 'a) * ('a -$>$ 'b) -$>$ 'c * 'b\\ |
|
350 val ||$>>$ : ('c * 'a) * ('a -$>$ 'd * 'b) -$>$ ('c * 'd) * 'b\\ |
|
351 val \#$>$ : ('a -$>$ 'b) * ('b -$>$ 'c) -$>$ 'a -$>$ 'c\\ |
|
352 val \#-$>$ : ('a -$>$ 'c * 'b) * ('c -$>$ 'b -$>$ 'd) -$>$ 'a -$>$ 'd\\ |
|
353 val \#$>>$ : ('a -$>$ 'c * 'b) * ('c -$>$ 'd) -$>$ 'a -$>$ 'd * 'b\\ |
|
354 val \#\#$>$ : ('a -$>$ 'c * 'b) * ('b -$>$ 'd) -$>$ 'a -$>$ 'c * 'd\\ |
|
355 val \#\#$>>$ : ('a -$>$ 'c * 'b) * ('b -$>$ 'e * 'd) -$>$ 'a -$>$ ('c * 'e) * 'd\\ |
|
356 } |
|
357 \end{itemize} |
|
358 \end{frame} |
|
359 |
|
360 \begin{frame} |
|
361 \frametitle{Example with combinators} |
|
362 \texttt{\footnotesize{ |
|
363 \begin{tabbing} |
|
364 xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill |
|
365 fun prep\_ori [] \_ \_ = ([], e\_ctxt)\\ |
|
366 \>| prep\_ori fmz thy pbt =\\ |
|
367 \>\>\>let\\ |
|
368 \>\>\>\>val ctxt = ProofContext.init\_global thy \\ |
|
369 \>\>\>\>\> |> fold declare\_constraints fmz\\ |
|
370 \>\>\>\>val ori = \\ |
|
371 \>\>\>\>\> map (add\_field thy pbt o split\_dts o the o parseNEW ctxt) fmz\\ |
|
372 \>\>\>\>\>\> |> add\_variants\\ |
|
373 \>\>\>\>val maxv = map fst ori |> max\\ |
|
374 \>\>\>\>val maxv = if maxv = 0 then 1 else maxv\\ |
|
375 \>\>\>\>val oris = coll\_variants ori\\ |
|
376 \>\>\>\>\> |> map (replace\_0 maxv |> apfst)\\ |
|
377 \>\>\>\>\> |> add\_id\\ |
|
378 \>\>\>\>\> |> map flattup\\ |
|
379 \>\>\>in (oris, ctxt) end; |
|
380 \end{tabbing} |
|
381 }} |
|
382 \dots which probably can be further polished. |
|
383 \end{frame} |
|
384 |
|
385 %\subsection[Future Development]{Preparation of Future Development} |
|
386 %\begin{frame} |
|
387 % \frametitle{Preparation of Future Development} |
|
388 % |
|
389 %% "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^ |
|
390 %% " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^ |
|
391 %% " (Try (Rewrite_Set Test_simplify False))) e_e; " ^ |
|
392 %% " (L_L::bool list) = " ^ |
|
393 %% " (SubProblem (Test', " ^ |
|
394 %% " [linear,univariate,equation,test]," ^ |
|
395 %% " [Test,solve_linear]) " ^ |
|
396 %% " [BOOL e_e, REAL v_v]) " ^ |
|
397 %% " in Check_elementwise L_L {(v_v::real). Assumptions}) " |
|
398 %\end{frame} |
|
399 % |
|
400 %\begin{frame} |
|
401 % \frametitle{Preparation of Future Development} |
|
402 % \begin{itemize} |
|
403 % \item logical data for Isabelle provers in contexts |
|
404 % \item \isac{} programming language more compact\\ |
|
405 % $\rightarrow$ context built automatically |
|
406 % \end{itemize} |
|
407 %\end{frame} |
|
408 |
|
409 |
|
410 \section[Problems]{Problems encountered in the project} |
|
411 \begin{frame} |
|
412 \frametitle{Problems encountered in the project} |
|
413 \begin{itemize} |
|
414 \item new Isabelle release in February 2011: update \sisac{} first |
|
415 \pause |
|
416 \item lines of code (LOC) in Isabelle and \sisac{}\\ \vspace{0.2cm} |
|
417 \textit{ |
|
418 \begin{tabular}{lrl} |
|
419 src/ & 1700 & $\,$k LOC\\ |
|
420 src/Pure/ & 70 & k LOC\\ |
|
421 src/Provers/ & 8 & k LOC\\ |
|
422 src/Tools/ & 800 & k LOC\\ |
|
423 src/Tools/isac/ & 37 & k LOC\\ |
|
424 src/Tools/isac/Knowledge & 16 & k LOC |
|
425 \end{tabular} |
|
426 } |
|
427 \pause |
|
428 \item changes scattered throughout the code ($\rightarrow$ grep) |
|
429 \pause |
|
430 \item documentation of Isabelle very ``technical'' (no API) |
|
431 \pause |
|
432 \item documentation of \sisac{} not up to date |
|
433 \end{itemize} |
|
434 \end{frame} |
|
435 |
|
436 %\begin{frame} |
|
437 % \frametitle{Lines of Code} |
|
438 % \begin{tabular}{lr} |
|
439 % src/ & 1700 k \\ |
|
440 % src/Pure/ & 70 k \\ |
|
441 % src/Provers/ & 8 k \\ |
|
442 % src/Tools/ & 800 k \\ |
|
443 % src/Tools/isac/ & 37 k \\ |
|
444 % src/Tools/isac/Knowledge & 16 k \\ |
|
445 % \end{tabular} |
|
446 %\end{frame} |
|
447 |
|
448 \section{Summary} |
|
449 \begin{frame} |
|
450 \frametitle{Summary} |
|
451 The project succeeded in all goals: |
|
452 \begin{itemize} |
|
453 \item implemented Isabelle's contexts in \sisac{} such that |
|
454 \item user input requires no type constraints anymore |
|
455 \item consistent logical data is prepared for Isabelle's provers |
|
456 \end{itemize} |
|
457 \pause |
|
458 The course of the project was close to the plan: |
|
459 \begin{itemize} |
|
460 \item faster in writing new code |
|
461 \item slower in integrating the code into \sisac |
|
462 \end{itemize} |
|
463 \pause |
|
464 The project provided essential prerequisites for further development of the Lucas-interpreter. |
|
465 \end{frame} |
|
466 |
|
467 \end{document} |
|
468 |
|
469 |
|