1 %!PS-Adobe-2.0 |
|
2 %%Creator: dot version 2.2 (Mon Sep 12 23:33:36 UTC 2005) |
|
3 %%For: (haftmann) Florian Haftmann |
|
4 %%Title: _anonymous_0 |
|
5 %%Pages: (atend) |
|
6 %%BoundingBox: 35 35 451 291 |
|
7 %%EndComments |
|
8 save |
|
9 %%BeginProlog |
|
10 /DotDict 200 dict def |
|
11 DotDict begin |
|
12 |
|
13 /setupLatin1 { |
|
14 mark |
|
15 /EncodingVector 256 array def |
|
16 EncodingVector 0 |
|
17 |
|
18 ISOLatin1Encoding 0 255 getinterval putinterval |
|
19 |
|
20 EncodingVector |
|
21 dup 306 /AE |
|
22 dup 301 /Aacute |
|
23 dup 302 /Acircumflex |
|
24 dup 304 /Adieresis |
|
25 dup 300 /Agrave |
|
26 dup 305 /Aring |
|
27 dup 303 /Atilde |
|
28 dup 307 /Ccedilla |
|
29 dup 311 /Eacute |
|
30 dup 312 /Ecircumflex |
|
31 dup 313 /Edieresis |
|
32 dup 310 /Egrave |
|
33 dup 315 /Iacute |
|
34 dup 316 /Icircumflex |
|
35 dup 317 /Idieresis |
|
36 dup 314 /Igrave |
|
37 dup 334 /Udieresis |
|
38 dup 335 /Yacute |
|
39 dup 376 /thorn |
|
40 dup 337 /germandbls |
|
41 dup 341 /aacute |
|
42 dup 342 /acircumflex |
|
43 dup 344 /adieresis |
|
44 dup 346 /ae |
|
45 dup 340 /agrave |
|
46 dup 345 /aring |
|
47 dup 347 /ccedilla |
|
48 dup 351 /eacute |
|
49 dup 352 /ecircumflex |
|
50 dup 353 /edieresis |
|
51 dup 350 /egrave |
|
52 dup 355 /iacute |
|
53 dup 356 /icircumflex |
|
54 dup 357 /idieresis |
|
55 dup 354 /igrave |
|
56 dup 360 /dcroat |
|
57 dup 361 /ntilde |
|
58 dup 363 /oacute |
|
59 dup 364 /ocircumflex |
|
60 dup 366 /odieresis |
|
61 dup 362 /ograve |
|
62 dup 365 /otilde |
|
63 dup 370 /oslash |
|
64 dup 372 /uacute |
|
65 dup 373 /ucircumflex |
|
66 dup 374 /udieresis |
|
67 dup 371 /ugrave |
|
68 dup 375 /yacute |
|
69 dup 377 /ydieresis |
|
70 |
|
71 % Set up ISO Latin 1 character encoding |
|
72 /starnetISO { |
|
73 dup dup findfont dup length dict begin |
|
74 { 1 index /FID ne { def }{ pop pop } ifelse |
|
75 } forall |
|
76 /Encoding EncodingVector def |
|
77 currentdict end definefont |
|
78 } def |
|
79 /Times-Roman starnetISO def |
|
80 /Times-Italic starnetISO def |
|
81 /Times-Bold starnetISO def |
|
82 /Times-BoldItalic starnetISO def |
|
83 /Helvetica starnetISO def |
|
84 /Helvetica-Oblique starnetISO def |
|
85 /Helvetica-Bold starnetISO def |
|
86 /Helvetica-BoldOblique starnetISO def |
|
87 /Courier starnetISO def |
|
88 /Courier-Oblique starnetISO def |
|
89 /Courier-Bold starnetISO def |
|
90 /Courier-BoldOblique starnetISO def |
|
91 cleartomark |
|
92 } bind def |
|
93 |
|
94 %%BeginResource: procset graphviz 0 0 |
|
95 /coord-font-family /Times-Roman def |
|
96 /default-font-family /Times-Roman def |
|
97 /coordfont coord-font-family findfont 8 scalefont def |
|
98 |
|
99 /InvScaleFactor 1.0 def |
|
100 /set_scale { |
|
101 dup 1 exch div /InvScaleFactor exch def |
|
102 dup scale |
|
103 } bind def |
|
104 |
|
105 % styles |
|
106 /solid { [] 0 setdash } bind def |
|
107 /dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def |
|
108 /dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def |
|
109 /invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def |
|
110 /bold { 2 setlinewidth } bind def |
|
111 /filled { } bind def |
|
112 /unfilled { } bind def |
|
113 /rounded { } bind def |
|
114 /diagonals { } bind def |
|
115 |
|
116 % hooks for setting color |
|
117 /nodecolor { sethsbcolor } bind def |
|
118 /edgecolor { sethsbcolor } bind def |
|
119 /graphcolor { sethsbcolor } bind def |
|
120 /nopcolor {pop pop pop} bind def |
|
121 |
|
122 /beginpage { % i j npages |
|
123 /npages exch def |
|
124 /j exch def |
|
125 /i exch def |
|
126 /str 10 string def |
|
127 npages 1 gt { |
|
128 gsave |
|
129 coordfont setfont |
|
130 0 0 moveto |
|
131 (\() show i str cvs show (,) show j str cvs show (\)) show |
|
132 grestore |
|
133 } if |
|
134 } bind def |
|
135 |
|
136 /set_font { |
|
137 findfont exch |
|
138 scalefont setfont |
|
139 } def |
|
140 |
|
141 % draw aligned label in bounding box aligned to current point |
|
142 /alignedtext { % width adj text |
|
143 /text exch def |
|
144 /adj exch def |
|
145 /width exch def |
|
146 gsave |
|
147 width 0 gt { |
|
148 text stringwidth pop adj mul 0 rmoveto |
|
149 } if |
|
150 [] 0 setdash |
|
151 text show |
|
152 grestore |
|
153 } def |
|
154 |
|
155 /boxprim { % xcorner ycorner xsize ysize |
|
156 4 2 roll |
|
157 moveto |
|
158 2 copy |
|
159 exch 0 rlineto |
|
160 0 exch rlineto |
|
161 pop neg 0 rlineto |
|
162 closepath |
|
163 } bind def |
|
164 |
|
165 /ellipse_path { |
|
166 /ry exch def |
|
167 /rx exch def |
|
168 /y exch def |
|
169 /x exch def |
|
170 matrix currentmatrix |
|
171 newpath |
|
172 x y translate |
|
173 rx ry scale |
|
174 0 0 1 0 360 arc |
|
175 setmatrix |
|
176 } bind def |
|
177 |
|
178 /endpage { showpage } bind def |
|
179 /showpage { } def |
|
180 |
|
181 /layercolorseq |
|
182 [ % layer color sequence - darkest to lightest |
|
183 [0 0 0] |
|
184 [.2 .8 .8] |
|
185 [.4 .8 .8] |
|
186 [.6 .8 .8] |
|
187 [.8 .8 .8] |
|
188 ] |
|
189 def |
|
190 |
|
191 /layerlen layercolorseq length def |
|
192 |
|
193 /setlayer {/maxlayer exch def /curlayer exch def |
|
194 layercolorseq curlayer 1 sub layerlen mod get |
|
195 aload pop sethsbcolor |
|
196 /nodecolor {nopcolor} def |
|
197 /edgecolor {nopcolor} def |
|
198 /graphcolor {nopcolor} def |
|
199 } bind def |
|
200 |
|
201 /onlayer { curlayer ne {invis} if } def |
|
202 |
|
203 /onlayers { |
|
204 /myupper exch def |
|
205 /mylower exch def |
|
206 curlayer mylower lt |
|
207 curlayer myupper gt |
|
208 or |
|
209 {invis} if |
|
210 } def |
|
211 |
|
212 /curlayer 0 def |
|
213 |
|
214 %%EndResource |
|
215 %%EndProlog |
|
216 %%BeginSetup |
|
217 14 default-font-family set_font |
|
218 1 setmiterlimit |
|
219 % /arrowlength 10 def |
|
220 % /arrowwidth 5 def |
|
221 |
|
222 % make sure pdfmark is harmless for PS-interpreters other than Distiller |
|
223 /pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse |
|
224 % make '<<' and '>>' safe on PS Level 1 devices |
|
225 /languagelevel where {pop languagelevel}{1} ifelse |
|
226 2 lt { |
|
227 userdict (<<) cvn ([) cvn load put |
|
228 userdict (>>) cvn ([) cvn load put |
|
229 } if |
|
230 |
|
231 %%EndSetup |
|
232 %%Page: 1 1 |
|
233 %%PageBoundingBox: 36 36 451 291 |
|
234 %%PageOrientation: Portrait |
|
235 gsave |
|
236 35 35 416 256 boxprim clip newpath |
|
237 36 36 translate |
|
238 0 0 1 beginpage |
|
239 0 0 translate 0 rotate |
|
240 [ /CropBox [36 36 451 291] /PAGES pdfmark |
|
241 0.000 0.000 0.000 graphcolor |
|
242 14.00 /Times-Roman set_font |
|
243 |
|
244 % theory |
|
245 gsave 10 dict begin |
|
246 newpath 93 254 moveto |
|
247 1 254 lineto |
|
248 1 214 lineto |
|
249 93 214 lineto |
|
250 closepath |
|
251 stroke |
|
252 gsave 10 dict begin |
|
253 8 237 moveto |
|
254 (Isabelle/HOL) |
|
255 [4.56 5.52 6.24 6.96 6.24 3.84 3.84 6.24 3.84 10.08 10.08 8.64] |
|
256 xshow |
|
257 16 221 moveto |
|
258 (Isar theory) |
|
259 [4.56 5.52 6.24 4.56 3.6 4.08 6.96 6.24 6.96 4.8 6.96] |
|
260 xshow |
|
261 end grestore |
|
262 end grestore |
|
263 |
|
264 % selection |
|
265 gsave 10 dict begin |
|
266 183 234 38 18 ellipse_path |
|
267 stroke |
|
268 gsave 10 dict begin |
|
269 158 229 moveto |
|
270 (selection) |
|
271 [5.52 6.24 3.84 6.24 6.24 3.84 3.84 6.96 6.96] |
|
272 xshow |
|
273 end grestore |
|
274 end grestore |
|
275 |
|
276 % theory -> selection |
|
277 newpath 94 234 moveto |
|
278 107 234 121 234 135 234 curveto |
|
279 stroke |
|
280 gsave 10 dict begin |
|
281 solid |
|
282 1 setlinewidth |
|
283 0.000 0.000 0.000 edgecolor |
|
284 newpath 135 238 moveto |
|
285 145 234 lineto |
|
286 135 231 lineto |
|
287 closepath |
|
288 fill |
|
289 0.000 0.000 0.000 edgecolor |
|
290 newpath 135 238 moveto |
|
291 145 234 lineto |
|
292 135 231 lineto |
|
293 closepath |
|
294 stroke |
|
295 end grestore |
|
296 |
|
297 % sml |
|
298 gsave 10 dict begin |
|
299 newpath 74 144 moveto |
|
300 20 144 lineto |
|
301 20 108 lineto |
|
302 74 108 lineto |
|
303 closepath |
|
304 stroke |
|
305 gsave 10 dict begin |
|
306 32 121 moveto |
|
307 (SML) |
|
308 [7.68 12.48 8.64] |
|
309 xshow |
|
310 end grestore |
|
311 end grestore |
|
312 |
|
313 % other |
|
314 gsave 10 dict begin |
|
315 gsave 10 dict begin |
|
316 41 67 moveto |
|
317 (...) |
|
318 [3.6 3.6 3.6] |
|
319 xshow |
|
320 end grestore |
|
321 end grestore |
|
322 |
|
323 % haskell |
|
324 gsave 10 dict begin |
|
325 newpath 77 36 moveto |
|
326 17 36 lineto |
|
327 17 0 lineto |
|
328 77 0 lineto |
|
329 closepath |
|
330 stroke |
|
331 gsave 10 dict begin |
|
332 25 13 moveto |
|
333 (Haskell) |
|
334 [10.08 6.24 5.52 6.72 6.24 3.84 3.84] |
|
335 xshow |
|
336 end grestore |
|
337 end grestore |
|
338 |
|
339 % preprocessing |
|
340 gsave 10 dict begin |
|
341 183 180 52 18 ellipse_path |
|
342 stroke |
|
343 gsave 10 dict begin |
|
344 143 175 moveto |
|
345 (preprocessing) |
|
346 [6.96 4.56 6.24 6.96 4.56 6.96 6.24 6.24 5.52 5.52 3.84 6.96 6.96] |
|
347 xshow |
|
348 end grestore |
|
349 end grestore |
|
350 |
|
351 % selection -> preprocessing |
|
352 newpath 183 216 moveto |
|
353 183 213 183 211 183 208 curveto |
|
354 stroke |
|
355 gsave 10 dict begin |
|
356 solid |
|
357 1 setlinewidth |
|
358 0.000 0.000 0.000 edgecolor |
|
359 newpath 187 208 moveto |
|
360 183 198 lineto |
|
361 180 208 lineto |
|
362 closepath |
|
363 fill |
|
364 0.000 0.000 0.000 edgecolor |
|
365 newpath 187 208 moveto |
|
366 183 198 lineto |
|
367 180 208 lineto |
|
368 closepath |
|
369 stroke |
|
370 end grestore |
|
371 |
|
372 % def_eqn |
|
373 gsave 10 dict begin |
|
374 newpath 403 198 moveto |
|
375 283 198 lineto |
|
376 283 162 lineto |
|
377 403 162 lineto |
|
378 closepath |
|
379 stroke |
|
380 gsave 10 dict begin |
|
381 291 175 moveto |
|
382 (defining equations) |
|
383 [6.96 6.24 4.8 3.84 6.96 3.84 6.96 6.96 3.6 6.24 6.72 6.96 6.24 3.84 3.84 6.96 6.96 5.52] |
|
384 xshow |
|
385 end grestore |
|
386 end grestore |
|
387 |
|
388 % preprocessing -> def_eqn |
|
389 newpath 236 180 moveto |
|
390 248 180 260 180 273 180 curveto |
|
391 stroke |
|
392 gsave 10 dict begin |
|
393 solid |
|
394 1 setlinewidth |
|
395 0.000 0.000 0.000 edgecolor |
|
396 newpath 273 184 moveto |
|
397 283 180 lineto |
|
398 273 177 lineto |
|
399 closepath |
|
400 fill |
|
401 0.000 0.000 0.000 edgecolor |
|
402 newpath 273 184 moveto |
|
403 283 180 lineto |
|
404 273 177 lineto |
|
405 closepath |
|
406 stroke |
|
407 end grestore |
|
408 |
|
409 % serialization |
|
410 gsave 10 dict begin |
|
411 183 72 47 18 ellipse_path |
|
412 stroke |
|
413 gsave 10 dict begin |
|
414 148 67 moveto |
|
415 (serialization) |
|
416 [5.52 6.24 4.8 3.84 6.24 3.84 3.84 6.24 6.24 3.84 3.84 6.96 6.96] |
|
417 xshow |
|
418 end grestore |
|
419 end grestore |
|
420 |
|
421 % serialization -> sml |
|
422 newpath 150 85 moveto |
|
423 129 93 104 103 83 111 curveto |
|
424 stroke |
|
425 gsave 10 dict begin |
|
426 solid |
|
427 1 setlinewidth |
|
428 0.000 0.000 0.000 edgecolor |
|
429 newpath 82 108 moveto |
|
430 74 115 lineto |
|
431 85 114 lineto |
|
432 closepath |
|
433 fill |
|
434 0.000 0.000 0.000 edgecolor |
|
435 newpath 82 108 moveto |
|
436 74 115 lineto |
|
437 85 114 lineto |
|
438 closepath |
|
439 stroke |
|
440 end grestore |
|
441 |
|
442 % serialization -> other |
|
443 gsave 10 dict begin |
|
444 dotted |
|
445 newpath 135 72 moveto |
|
446 119 72 100 72 84 72 curveto |
|
447 stroke |
|
448 gsave 10 dict begin |
|
449 solid |
|
450 1 setlinewidth |
|
451 0.000 0.000 0.000 edgecolor |
|
452 newpath 84 69 moveto |
|
453 74 72 lineto |
|
454 84 76 lineto |
|
455 closepath |
|
456 fill |
|
457 0.000 0.000 0.000 edgecolor |
|
458 newpath 84 69 moveto |
|
459 74 72 lineto |
|
460 84 76 lineto |
|
461 closepath |
|
462 stroke |
|
463 end grestore |
|
464 end grestore |
|
465 |
|
466 % serialization -> haskell |
|
467 newpath 150 59 moveto |
|
468 131 51 107 42 86 34 curveto |
|
469 stroke |
|
470 gsave 10 dict begin |
|
471 solid |
|
472 1 setlinewidth |
|
473 0.000 0.000 0.000 edgecolor |
|
474 newpath 88 31 moveto |
|
475 77 30 lineto |
|
476 85 37 lineto |
|
477 closepath |
|
478 fill |
|
479 0.000 0.000 0.000 edgecolor |
|
480 newpath 88 31 moveto |
|
481 77 30 lineto |
|
482 85 37 lineto |
|
483 closepath |
|
484 stroke |
|
485 end grestore |
|
486 |
|
487 % translation |
|
488 gsave 10 dict begin |
|
489 343 126 43 18 ellipse_path |
|
490 stroke |
|
491 gsave 10 dict begin |
|
492 313 121 moveto |
|
493 (translation) |
|
494 [3.84 4.56 6.24 6.96 5.52 3.84 6.24 3.84 3.84 6.96 6.96] |
|
495 xshow |
|
496 end grestore |
|
497 end grestore |
|
498 |
|
499 % def_eqn -> translation |
|
500 newpath 343 162 moveto |
|
501 343 159 343 157 343 154 curveto |
|
502 stroke |
|
503 gsave 10 dict begin |
|
504 solid |
|
505 1 setlinewidth |
|
506 0.000 0.000 0.000 edgecolor |
|
507 newpath 347 154 moveto |
|
508 343 144 lineto |
|
509 340 154 lineto |
|
510 closepath |
|
511 fill |
|
512 0.000 0.000 0.000 edgecolor |
|
513 newpath 347 154 moveto |
|
514 343 144 lineto |
|
515 340 154 lineto |
|
516 closepath |
|
517 stroke |
|
518 end grestore |
|
519 |
|
520 % iml |
|
521 gsave 10 dict begin |
|
522 newpath 413 90 moveto |
|
523 273 90 lineto |
|
524 273 54 lineto |
|
525 413 54 lineto |
|
526 closepath |
|
527 stroke |
|
528 gsave 10 dict begin |
|
529 280 67 moveto |
|
530 (intermediate language) |
|
531 [3.84 6.96 3.84 6.24 4.8 10.8 6.24 6.96 3.84 6.24 3.84 6.24 3.6 3.84 6.24 6.96 6.96 6.96 6.24 6.72 6.24] |
|
532 xshow |
|
533 end grestore |
|
534 end grestore |
|
535 |
|
536 % translation -> iml |
|
537 newpath 343 108 moveto |
|
538 343 105 343 103 343 100 curveto |
|
539 stroke |
|
540 gsave 10 dict begin |
|
541 solid |
|
542 1 setlinewidth |
|
543 0.000 0.000 0.000 edgecolor |
|
544 newpath 347 100 moveto |
|
545 343 90 lineto |
|
546 340 100 lineto |
|
547 closepath |
|
548 fill |
|
549 0.000 0.000 0.000 edgecolor |
|
550 newpath 347 100 moveto |
|
551 343 90 lineto |
|
552 340 100 lineto |
|
553 closepath |
|
554 stroke |
|
555 end grestore |
|
556 |
|
557 % iml -> serialization |
|
558 newpath 272 72 moveto |
|
559 262 72 251 72 241 72 curveto |
|
560 stroke |
|
561 gsave 10 dict begin |
|
562 solid |
|
563 1 setlinewidth |
|
564 0.000 0.000 0.000 edgecolor |
|
565 newpath 241 69 moveto |
|
566 231 72 lineto |
|
567 241 76 lineto |
|
568 closepath |
|
569 fill |
|
570 0.000 0.000 0.000 edgecolor |
|
571 newpath 241 69 moveto |
|
572 231 72 lineto |
|
573 241 76 lineto |
|
574 closepath |
|
575 stroke |
|
576 end grestore |
|
577 endpage |
|
578 showpage |
|
579 grestore |
|
580 %%PageTrailer |
|
581 %%EndPage: 1 |
|
582 %%Trailer |
|
583 %%Pages: 1 |
|
584 end |
|
585 restore |
|
586 %%EOF |
|