wneuper/isa: doc-src/gfx/Isa-logics.eps@20e3616b2d9c

     1 %!PS-Adobe-3.0 EPSF-3.0

     2 %%BoundingBox: 106 651 274 788

     3 %%Title: (Isa-logics)

     4 %%Creator: (ClarisDraw: LaserWriter 8 8.1.1)

     5 %%CreationDate: (9:19 pm Wednesday, April 24, 1996)

     6 %%For: (Larry)

     7 %%Pages: 1

     8 %%DocumentFonts: Times-Roman

     9 %%DocumentNeededFonts: Times-Roman

    10 %%DocumentSuppliedFonts:

    11 %%DocumentData: Clean7Bit

    12 %%PageOrder: Ascend

    13 %%Orientation: Portrait

    14 %ADO_PaperArea: -124 -112 3244 2268

    15 %ADO_ImageableArea: 0 0 3124 2152

    16 %%EndComments

    17 /md 148 dict def md begin

    18 /currentpacking where {pop /sc_oldpacking currentpacking def true setpacking}if

    19 %%BeginFile: adobe_psp_basic

    20 %%Copyright: Copyright 1990-1993 Adobe Systems Incorporated. All Rights Reserved.

    21 /bd{bind def}bind def

    22 /xdf{exch def}bd

    23 /xs{exch store}bd

    24 /ld{load def}bd

    25 /Z{0 def}bd

    26 /T/true

    27 /F/false

    28 /:L/lineto

    29 /lw/setlinewidth

    30 /:M/moveto

    31 /rl/rlineto

    32 /rm/rmoveto

    33 /:C/curveto

    34 /:T/translate

    35 /:K/closepath

    36 /:mf/makefont

    37 /gS/gsave

    38 /gR/grestore

    39 /np/newpath

    40 14{ld}repeat

    41 /$m matrix def

    42 /av 81 def

    43 /por true def

    44 /normland false def

    45 /psb-nosave{}bd

    46 /pse-nosave{}bd

    47 /us Z

    48 /psb{/us save store}bd

    49 /pse{us restore}bd

    50 /level2

    51 /languagelevel where

    52 {

    53 pop languagelevel 2 ge

    54 }{

    55 false

    56 }ifelse

    57 def

    58 /featurecleanup

    59 {

    60 stopped

    61 cleartomark

    62 countdictstack exch sub dup 0 gt

    63 {

    64 {end}repeat

    65 }{

    66 pop

    67 }ifelse

    68 }bd

    69 /noload Z

    70 /startnoload

    71 {

    72 {/noload save store}if

    73 }bd

    74 /endnoload

    75 {

    76 {noload restore}if

    77 }bd

    78 level2 startnoload

    79 /setjob

    80 {

    81 statusdict/jobname 3 -1 roll put

    82 }bd

    83 /setcopies

    84 {

    85 userdict/#copies 3 -1 roll put

    86 }bd

    87 level2 endnoload level2 not startnoload

    88 /setjob

    89 {

    90 1 dict begin/JobName xdf currentdict end setuserparams

    91 }bd

    92 /setcopies

    93 {

    94 1 dict begin/NumCopies xdf currentdict end setpagedevice

    95 }bd

    96 level2 not endnoload

    97 /pm Z

    98 /mT Z

    99 /sD Z

   100 /realshowpage Z

   101 /initializepage

   102 {

   103 /pm save store mT concat

   104 }bd

   105 /endp

   106 {

   107 pm restore showpage

   108 }def

   109 /$c/DeviceRGB def

   110 /rectclip where

   111 {

   112 pop/rC/rectclip ld

   113 }{

   114 /rC

   115 {

   116 np 4 2 roll

   117 :M

   118 1 index 0 rl

   119 0 exch rl

   120 neg 0 rl

   121 :K

   122 clip np

   123 }bd

   124 }ifelse

   125 /rectfill where

   126 {

   127 pop/rF/rectfill ld

   128 }{

   129 /rF

   130 {

   131 gS

   132 np

   133 4 2 roll

   134 :M

   135 1 index 0 rl

   136 0 exch rl

   137 neg 0 rl

   138 fill

   139 gR

   140 }bd

   141 }ifelse

   142 /rectstroke where

   143 {

   144 pop/rS/rectstroke ld

   145 }{

   146 /rS

   147 {

   148 gS

   149 np

   150 4 2 roll

   151 :M

   152 1 index 0 rl

   153 0 exch rl

   154 neg 0 rl

   155 :K

   156 stroke

   157 gR

   158 }bd

   159 }ifelse

   160 %%EndFile

   161 %%BeginFile: adobe_psp_colorspace_level1

   162 %%Copyright: Copyright 1991-1993 Adobe Systems Incorporated. All Rights Reserved.

   163 /G/setgray ld

   164 /:F/setrgbcolor ld

   165 %%EndFile

   166 %%BeginFile: adobe_psp_uniform_graphics

   167 %%Copyright: Copyright 1990-1993 Adobe Systems Incorporated. All Rights Reserved.

   168 /@a

   169 {

   170 np :M 0 rl :L 0 exch rl 0 rl :L fill

   171 }bd

   172 /@b

   173 {

   174 np :M 0 rl 0 exch rl :L 0 rl 0 exch rl fill

   175 }bd

   176 /arct where

   177 {

   178 pop

   179 }{

   180 /arct

   181 {

   182 arcto pop pop pop pop

   183 }bd

   184 }ifelse

   185 /x1 Z

   186 /x2 Z

   187 /y1 Z

   188 /y2 Z

   189 /rad Z

   190 /@q

   191 {

   192 /rad xs

   193 /y2 xs

   194 /x2 xs

   195 /y1 xs

   196 /x1 xs

   197 np

   198 x2 x1 add 2 div y1 :M

   199 x2 y1 x2 y2 rad arct

   200 x2 y2 x1 y2 rad arct

   201 x1 y2 x1 y1 rad arct

   202 x1 y1 x2 y1 rad arct

   203 fill

   204 }bd

   205 /@s

   206 {

   207 /rad xs

   208 /y2 xs

   209 /x2 xs

   210 /y1 xs

   211 /x1 xs

   212 np

   213 x2 x1 add 2 div y1 :M

   214 x2 y1 x2 y2 rad arct

   215 x2 y2 x1 y2 rad arct

   216 x1 y2 x1 y1 rad arct

   217 x1 y1 x2 y1 rad arct

   218 :K

   219 stroke

   220 }bd

   221 /@i

   222 {

   223 np 0 360 arc fill

   224 }bd

   225 /@j

   226 {

   227 gS

   228 np

   229 :T

   230 scale

   231 0 0 .5 0 360 arc

   232 fill

   233 gR

   234 }bd

   235 /@e

   236 {

   237 np

   238 0 360 arc

   239 :K

   240 stroke

   241 }bd

   242 /@f

   243 {

   244 np

   245 $m currentmatrix

   246 pop

   247 :T

   248 scale

   249 0 0 .5 0 360 arc

   250 :K

   251 $m setmatrix

   252 stroke

   253 }bd

   254 /@k

   255 {

   256 gS

   257 np

   258 :T

   259 0 0 :M

   260 0 0 5 2 roll

   261 arc fill

   262 gR

   263 }bd

   264 /@l

   265 {

   266 gS

   267 np

   268 :T

   269 0 0 :M

   270 scale

   271 0 0 .5 5 -2 roll arc

   272 fill

   273 gR

   274 }bd

   275 /@m

   276 {

   277 np

   278 arc

   279 stroke

   280 }bd

   281 /@n

   282 {

   283 np

   284 $m currentmatrix

   285 pop

   286 :T

   287 scale

   288 0 0 .5 5 -2 roll arc

   289 $m setmatrix

   290 stroke

   291 }bd

   292 %%EndFile

   293 %%BeginFile: adobe_psp_customps

   294 %%Copyright: Copyright 1990-1993 Adobe Systems Incorporated. All Rights Reserved.

   295 /$t Z

   296 /$p Z

   297 /$s Z

   298 /$o 1. def

   299 /2state? false def

   300 /ps Z

   301 level2 startnoload

   302 /pushcolor/currentrgbcolor ld

   303 /popcolor/setrgbcolor ld

   304 /setcmykcolor where

   305 {

   306 pop/currentcmykcolor where

   307 {

   308 pop/pushcolor/currentcmykcolor ld

   309 /popcolor/setcmykcolor ld

   310 }if

   311 }if

   312 level2 endnoload level2 not startnoload

   313 /pushcolor

   314 {

   315 currentcolorspace $c eq

   316 {

   317 currentcolor currentcolorspace true

   318 }{

   319 currentcmykcolor false

   320 }ifelse

   321 }bd

   322 /popcolor

   323 {

   324 {

   325 setcolorspace setcolor

   326 }{

   327 setcmykcolor

   328 }ifelse

   329 }bd

   330 level2 not endnoload

   331 /pushstatic

   332 {

   333 ps

   334 2state?

   335 $o

   336 $t

   337 $p

   338 $s

   339 }bd

   340 /popstatic

   341 {

   342 /$s xs

   343 /$p xs

   344 /$t xs

   345 /$o xs

   346 /2state? xs

   347 /ps xs

   348 }bd

   349 /pushgstate

   350 {

   351 save errordict/nocurrentpoint{pop 0 0}put

   352 currentpoint

   353 3 -1 roll restore

   354 pushcolor

   355 currentlinewidth

   356 currentlinecap

   357 currentlinejoin

   358 currentdash exch aload length

   359 np clippath pathbbox

   360 $m currentmatrix aload pop

   361 }bd

   362 /popgstate

   363 {

   364 $m astore setmatrix

   365 2 index sub exch

   366 3 index sub exch

   367 rC

   368 array astore exch setdash

   369 setlinejoin

   370 setlinecap

   371 lw

   372 popcolor

   373 np :M

   374 }bd

   375 /bu

   376 {

   377 pushgstate

   378 gR

   379 pushgstate

   380 2state?

   381 {

   382 gR

   383 pushgstate

   384 }if

   385 pushstatic

   386 pm restore

   387 mT concat

   388 }bd

   389 /bn

   390 {

   391 /pm save store

   392 popstatic

   393 popgstate

   394 gS

   395 popgstate

   396 2state?

   397 {

   398 gS

   399 popgstate

   400 }if

   401 }bd

   402 /cpat{pop 64 div G 8{pop}repeat}bd

   403 %%EndFile

   404 %%BeginFile: adobe_psp_basic_text

   405 %%Copyright: Copyright 1990-1993 Adobe Systems Incorporated. All Rights Reserved.

   406 /S/show ld

   407 /A{

   408 0.0 exch ashow

   409 }bd

   410 /R{

   411 0.0 exch 32 exch widthshow

   412 }bd

   413 /W{

   414 0.0 3 1 roll widthshow

   415 }bd

   416 /J{

   417 0.0 32 4 2 roll 0.0 exch awidthshow

   418 }bd

   419 /V{

   420 0.0 4 1 roll 0.0 exch awidthshow

   421 }bd

   422 /fcflg true def

   423 /fc{

   424 fcflg{

   425 vmstatus exch sub 50000 lt{

   426 (%%[ Warning: Running out of memory ]%%\r)print flush/fcflg false store

   427 }if pop

   428 }if

   429 }bd

   430 /$f[1 0 0 -1 0 0]def

   431 /:ff{$f :mf}bd

   432 /MacEncoding StandardEncoding 256 array copy def

   433 MacEncoding 39/quotesingle put

   434 MacEncoding 96/grave put

   435 /Adieresis/Aring/Ccedilla/Eacute/Ntilde/Odieresis/Udieresis/aacute

   436 /agrave/acircumflex/adieresis/atilde/aring/ccedilla/eacute/egrave

   437 /ecircumflex/edieresis/iacute/igrave/icircumflex/idieresis/ntilde/oacute

   438 /ograve/ocircumflex/odieresis/otilde/uacute/ugrave/ucircumflex/udieresis

   439 /dagger/degree/cent/sterling/section/bullet/paragraph/germandbls

   440 /registered/copyright/trademark/acute/dieresis/notequal/AE/Oslash

   441 /infinity/plusminus/lessequal/greaterequal/yen/mu/partialdiff/summation

   442 /product/pi/integral/ordfeminine/ordmasculine/Omega/ae/oslash

   443 /questiondown/exclamdown/logicalnot/radical/florin/approxequal/Delta/guillemotleft

   444 /guillemotright/ellipsis/space/Agrave/Atilde/Otilde/OE/oe

   445 /endash/emdash/quotedblleft/quotedblright/quoteleft/quoteright/divide/lozenge

   446 /ydieresis/Ydieresis/fraction/currency/guilsinglleft/guilsinglright/fi/fl

   447 /daggerdbl/periodcentered/quotesinglbase/quotedblbase/perthousand

   448 /Acircumflex/Ecircumflex/Aacute/Edieresis/Egrave/Iacute/Icircumflex/Idieresis/Igrave

   449 /Oacute/Ocircumflex/apple/Ograve/Uacute/Ucircumflex/Ugrave/dotlessi/circumflex/tilde

   450 /macron/breve/dotaccent/ring/cedilla/hungarumlaut/ogonek/caron

   451 MacEncoding 128 128 getinterval astore pop

   452 level2 startnoload

   453 /copyfontdict

   454 {

   455 findfont dup length dict

   456 begin

   457 {

   458 1 index/FID ne{def}{pop pop}ifelse

   459 }forall

   460 }bd

   461 level2 endnoload level2 not startnoload

   462 /copyfontdict

   463 {

   464 findfont dup length dict

   465 copy

   466 begin

   467 }bd

   468 level2 not endnoload

   469 md/fontname known not{

   470 /fontname/customfont def

   471 }if

   472 /Encoding Z

   473 /:mre

   474 {

   475 copyfontdict

   476 /Encoding MacEncoding def

   477 fontname currentdict

   478 end

   479 definefont :ff def

   480 }bd

   481 /:bsr

   482 {

   483 copyfontdict

   484 /Encoding Encoding 256 array copy def

   485 Encoding dup

   486 }bd

   487 /pd{put dup}bd

   488 /:esr

   489 {

   490 pop pop

   491 fontname currentdict

   492 end

   493 definefont :ff def

   494 }bd

   495 /scf

   496 {

   497 scalefont def

   498 }bd

   499 /scf-non

   500 {

   501 $m scale :mf setfont

   502 }bd

   503 /ps Z

   504 /fz{/ps xs}bd

   505 /sf/setfont ld

   506 /cF/currentfont ld

   507 /mbf

   508 {

   509 /makeblendedfont where

   510 {

   511 pop

   512 makeblendedfont

   513 /ABlend exch definefont

   514 }{

   515 pop

   516 }ifelse

   517 def

   518 }def

   519 %%EndFile

   520 /currentpacking where {pop sc_oldpacking setpacking}if

   521 end		% md

   522 %%EndProlog

   523 %%BeginSetup

   524 md begin

   525 /pT[1 0 0 -1 28 811]def/mT[.25 0 0 -.25 28 811]def

   526 /sD 16 dict def

   527 %%IncludeFont: Times-Roman

   528 /f0_1/Times-Roman :mre

   529 /f0_40 f0_1 40 scf

   530 /Courier findfont[10 0 0 -10 0 0]:mf setfont

   531 %PostScript Hack by Mike Brors 12/7/90

   532 /DisableNextSetRGBColor

   533 	{

   534 	userdict begin

   535 	/setrgbcolor

   536 		{

   537 		pop

   538 		pop

   539 		pop

   540 		userdict begin

   541 		/setrgbcolor systemdict /setrgbcolor get def

   542 		end

   543 		} def

   544 	end

   545 } bind def

   546 /bcarray where {

   547 	pop

   548 	bcarray 2 {

   549 		/da 4 ps div def

   550 		df setfont gsave cs wi

   551 		1 index 0 ne{exch da add exch}if grestore setcharwidth

   552 		cs 0 0 smc da 0 smc da da smc 0 da smc c

   553 		gray

   554 		{ gl}

   555 		{1 setgray}ifelse

   556 		da 2. div dup moveto show

   557 	}bind put

   558 } if

   559 %

   560 % Used to snap to device pixels, 1/4th of the pixel in.

   561 /stp {  % x y  pl  x y                % Snap To Pixel, pixel  (auto stroke adjust)

   562 	transform

   563 	0.25 sub round 0.25 add exch

   564 	0.25 sub round 0.25 add exch

   565 	itransform

   566 } bind def

   568 /snapmoveto { % x y  m  -             % moveto, auto stroke adjust

   569 	stp  moveto

   570 } bind def

   572 /snaplineto { % x y  l  -             % lineto, auto stroke adjust

   573 	stp lineto

   574 } bind def

   575 %%EndSetup

   576 %%Page: 1 1

   577 %%BeginPageSetup

   578 initializepage

   579 %%EndPageSetup

   580 gS 0 0 2152 3124 rC

   581 0 0 :M

   582 .25 0 translate

   583 /DrawObject_save_matrix_0 matrix currentmatrix def

   584 0 0 2152 2912 rC

   585 -40 -12 :M

   586 DrawObject_save_matrix_0 setmatrix

   587 /DrawObject_save_matrix_0 matrix currentmatrix def

   588 -40 -12 :M

   589 /DrawObject_save_matrix_1 matrix currentmatrix def

   590 0 0 2152 2911 rC

   591 -40 -12 :M

   592 /DrawObject_save_matrix_2 matrix currentmatrix def

   593 -40 -12 :M

   594 DrawObject_save_matrix_2 setmatrix

   595 DrawObject_save_matrix_1 setmatrix

   596 /DrawObject_save_matrix_1 matrix currentmatrix def

   597 558 556 208 48 rC

   598 558 556 :M

   599 DrawObject_save_matrix_1 setmatrix

   600 /DrawObject_save_matrix_1 matrix currentmatrix def

   601 gR

   602 gS 553 520 218 84 rC

   603 558 592 :M

   604 f0_40 sf

   605 -.055(Pure Isabelle)A

   606 gR

   607 gS 0 0 2152 2912 rC

   608 4 lw

   609 518 528 806 636 32 @s

   610 168 24 :M

   611 DrawObject_save_matrix_1 setmatrix

   612 /DrawObject_save_matrix_1 matrix currentmatrix def

   613 426 422 -4 4 538 526 4 426 418 @a

   614 426 418 :M

   615 DrawObject_save_matrix_1 setmatrix

   616 /DrawObject_save_matrix_1 matrix currentmatrix def

   617 -4 -4 790 530 4 4 894 418 @b

   618 786 526 :M

   619 DrawObject_save_matrix_1 setmatrix

   620 /DrawObject_save_matrix_1 matrix currentmatrix def

   621 588 422 -4 4 610 526 4 588 418 @a

   622 588 418 :M

   623 DrawObject_save_matrix_1 setmatrix

   624 /DrawObject_save_matrix_1 matrix currentmatrix def

   625 -4 -4 718 530 4 4 732 418 @b

   626 714 526 :M

   627 DrawObject_save_matrix_1 setmatrix

   628 /DrawObject_save_matrix_1 matrix currentmatrix def

   629 376 364 92 48 rC

   630 376 364 :M

   631 DrawObject_save_matrix_1 setmatrix

   632 /DrawObject_save_matrix_1 matrix currentmatrix def

   633 gR

   634 gS 371 328 102 84 rC

   635 376 400 :M

   636 f0_40 sf

   637 -.286(IFOL)A

   638 gR

   639 gS 556 364 76 48 rC

   640 556 364 :M

   641 DrawObject_save_matrix_1 setmatrix

   642 /DrawObject_save_matrix_1 matrix currentmatrix def

   643 gR

   644 gS 551 328 86 84 rC

   645 556 400 :M

   646 f0_40 sf

   647 -.273(CTT)A

   648 gR

   649 gS 700 364 84 48 rC

   650 700 364 :M

   651 DrawObject_save_matrix_1 setmatrix

   652 /DrawObject_save_matrix_1 matrix currentmatrix def

   653 gR

   654 gS 695 328 94 84 rC

   655 700 400 :M

   656 f0_40 sf

   657 -.094(HOL)A

   658 gR

   659 gS 880 364 56 48 rC

   660 880 364 :M

   661 DrawObject_save_matrix_1 setmatrix

   662 /DrawObject_save_matrix_1 matrix currentmatrix def

   663 gR

   664 gS 875 328 66 84 rC

   665 880 400 :M

   666 f0_40 sf

   667 -.311(LK)A

   668 gR

   669 gS 0 0 2152 2912 rC

   670 -4 -4 916 361 4 4 912 285 @b

   671 4 lw

   672 912 357 :M

   673 DrawObject_save_matrix_1 setmatrix

   674 /DrawObject_save_matrix_1 matrix currentmatrix def

   675 320 94 :M

   676 /DrawObject_save_matrix_2 matrix currentmatrix def

   677 336 152 -4 4 394 220 4 336 148 @a

   678 336 148 :M

   679 DrawObject_save_matrix_2 setmatrix

   680 /DrawObject_save_matrix_2 matrix currentmatrix def

   681 -4 -4 430 224 4 4 480 148 @b

   682 426 220 :M

   683 DrawObject_save_matrix_2 setmatrix

   684 /DrawObject_save_matrix_2 matrix currentmatrix def

   685 320 94 48 48 rC

   686 320 94 :M

   687 DrawObject_save_matrix_2 setmatrix

   688 /DrawObject_save_matrix_2 matrix currentmatrix def

   689 gR

   690 gS 315 58 58 84 rC

   691 320 130 :M

   692 f0_40 sf

   693 -.67(ZF)A

   694 gR

   695 gS 448 94 76 48 rC

   696 448 94 :M

   697 DrawObject_save_matrix_2 setmatrix

   698 DrawObject_save_matrix_1 setmatrix

   699 /DrawObject_save_matrix_1 matrix currentmatrix def

   700 gR

   701 gS 443 58 86 84 rC

   702 448 130 :M

   703 f0_40 sf

   704 -.175(LCF)A

   705 gR

   706 gS 860 178 116 96 rC

   707 gR

   708 gS 855 142 126 132 rC

   709 860 214 :M

   710 f0_40 sf

   711 -.106(Modal)A

   712 975 262 :M

   713 DrawObject_save_matrix_1 setmatrix

   714 /DrawObject_save_matrix_1 matrix currentmatrix def

   715 860 262 :M

   716 -.077(  logics)A

   717 gR

   718 gS 0 0 2152 2912 rC

   719 -4 -4 412 360 4 4 408 284 @b

   720 4 lw

   721 408 356 :M

   722 DrawObject_save_matrix_1 setmatrix

   723 /DrawObject_save_matrix_1 matrix currentmatrix def

   724 376 228 76 48 rC

   725 376 228 :M

   726 DrawObject_save_matrix_1 setmatrix

   727 /DrawObject_save_matrix_1 matrix currentmatrix def

   728 gR

   729 gS 371 192 86 84 rC

   730 376 264 :M

   731 f0_40 sf

   732 -.273(FOL)A

   733 gR

   734 gS 680 230 132 48 rC

   735 680 230 :M

   736 DrawObject_save_matrix_1 setmatrix

   737 /DrawObject_save_matrix_1 matrix currentmatrix def

   738 gR

   739 gS 675 194 142 84 rC

   740 680 266 :M

   741 f0_40 sf

   742 -.026(HOLCF)A

   743 gR

   744 gS 0 0 2152 2912 rC

   745 -4 -4 748 361 4 4 744 285 @b

   746 4 lw

   747 744 357 :M

   748 DrawObject_save_matrix_1 setmatrix

   749 DrawObject_save_matrix_0 setmatrix

   750 endp

   751 %%Trailer

   752 end		% md

   753 %%EOF

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 5374	6ef3742b6153
permissions	-rw-r--r--