%!PS-Adobe-3.0 EPSF-3.0

%%BoundingBox: 106 651 274 788

%%Title: (Isa-logics)

%%Creator: (ClarisDraw: LaserWriter 8 8.1.1)

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

%%For: (Larry)

%%Pages: 1

%%DocumentFonts: Times-Roman

%%DocumentNeededFonts: Times-Roman

%%DocumentSuppliedFonts:

%%DocumentData: Clean7Bit

%%PageOrder: Ascend

%%Orientation: Portrait

%ADO_PaperArea: -124 -112 3244 2268

%ADO_ImageableArea: 0 0 3124 2152

%%EndComments

/md 148 dict def md begin

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

%%BeginFile: adobe_psp_basic

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

/bd{bind def}bind def

/xdf{exch def}bd

/xs{exch store}bd

/ld{load def}bd

/Z{0 def}bd

/T/true

/F/false

/:L/lineto

/lw/setlinewidth

/:M/moveto

/rl/rlineto

/rm/rmoveto

/:C/curveto

/:T/translate

/:K/closepath

/:mf/makefont

/gS/gsave

/gR/grestore

/np/newpath

14{ld}repeat

/$m matrix def

/av 81 def

/por true def

/normland false def

/psb-nosave{}bd

/pse-nosave{}bd

/us Z

/psb{/us save store}bd

/pse{us restore}bd

/level2

/languagelevel where

{

pop languagelevel 2 ge

}{

false

}ifelse

def

/featurecleanup

{

stopped

cleartomark

countdictstack exch sub dup 0 gt

{

{end}repeat

}{

pop

}ifelse

}bd

/noload Z

/startnoload

{

{/noload save store}if

}bd

/endnoload

{

{noload restore}if

}bd

level2 startnoload

/setjob

{

statusdict/jobname 3 -1 roll put

}bd

/setcopies

{

userdict/#copies 3 -1 roll put

}bd

level2 endnoload level2 not startnoload

/setjob

{

1 dict begin/JobName xdf currentdict end setuserparams

}bd

/setcopies

{

1 dict begin/NumCopies xdf currentdict end setpagedevice

}bd

level2 not endnoload

/pm Z

/mT Z

/sD Z

/realshowpage Z

/initializepage

{

/pm save store mT concat

}bd

/endp

{

pm restore showpage

}def

/$c/DeviceRGB def

/rectclip where

{

pop/rC/rectclip ld

}{

/rC

{

np 4 2 roll

:M

1 index 0 rl

0 exch rl

neg 0 rl

:K

clip np

}bd

}ifelse

/rectfill where

{

pop/rF/rectfill ld

}{

/rF

{

gS

np

4 2 roll

:M

1 index 0 rl

0 exch rl

neg 0 rl

fill

gR

}bd

}ifelse

/rectstroke where

{

pop/rS/rectstroke ld

}{

/rS

{

gS

np

4 2 roll

:M

1 index 0 rl

0 exch rl

neg 0 rl

:K

stroke

gR

}bd

}ifelse

%%EndFile

%%BeginFile: adobe_psp_colorspace_level1

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

/G/setgray ld

/:F/setrgbcolor ld

%%EndFile

%%BeginFile: adobe_psp_uniform_graphics

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

/@a

{

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

}bd

/@b

{

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

}bd

/arct where

{

pop

}{

/arct

{

arcto pop pop pop pop

}bd

}ifelse

/x1 Z

/x2 Z

/y1 Z

/y2 Z

/rad Z

/@q

{

/rad xs

/y2 xs

/x2 xs

/y1 xs

/x1 xs

np

x2 x1 add 2 div y1 :M

x2 y1 x2 y2 rad arct

x2 y2 x1 y2 rad arct

x1 y2 x1 y1 rad arct

x1 y1 x2 y1 rad arct

fill

}bd

/@s

{

/rad xs

/y2 xs

/x2 xs

/y1 xs

/x1 xs

np

x2 x1 add 2 div y1 :M

x2 y1 x2 y2 rad arct

x2 y2 x1 y2 rad arct

x1 y2 x1 y1 rad arct

x1 y1 x2 y1 rad arct

:K

stroke

}bd

/@i

{

np 0 360 arc fill

}bd

/@j

{

gS

np

:T

scale

0 0 .5 0 360 arc

fill

gR

}bd

/@e

{

np

0 360 arc

:K

stroke

}bd

/@f

{

np

$m currentmatrix

pop

:T

scale

0 0 .5 0 360 arc

:K

$m setmatrix

stroke

}bd

/@k

{

gS

np

:T

0 0 :M

0 0 5 2 roll

arc fill

gR

}bd

/@l

{

gS

np

:T

0 0 :M

scale

0 0 .5 5 -2 roll arc

fill

gR

}bd

/@m

{

np

arc

stroke

}bd

/@n

{

np

$m currentmatrix

pop

:T

scale

0 0 .5 5 -2 roll arc

$m setmatrix

stroke

}bd

%%EndFile

%%BeginFile: adobe_psp_customps

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

/$t Z

/$p Z

/$s Z

/$o 1. def

/2state? false def

/ps Z

level2 startnoload

/pushcolor/currentrgbcolor ld

/popcolor/setrgbcolor ld

/setcmykcolor where

{

pop/currentcmykcolor where

{

pop/pushcolor/currentcmykcolor ld

/popcolor/setcmykcolor ld

}if

}if

level2 endnoload level2 not startnoload

/pushcolor

{

currentcolorspace $c eq

{

currentcolor currentcolorspace true

}{

currentcmykcolor false

}ifelse

}bd

/popcolor

{

{

setcolorspace setcolor

}{

setcmykcolor

}ifelse

}bd

level2 not endnoload

/pushstatic

{

ps

2state?

$o

$t

$p

$s

}bd

/popstatic

{

/$s xs

/$p xs

/$t xs

/$o xs

/2state? xs

/ps xs

}bd

/pushgstate

{

save errordict/nocurrentpoint{pop 0 0}put

currentpoint

3 -1 roll restore

pushcolor

currentlinewidth

currentlinecap

currentlinejoin

currentdash exch aload length

np clippath pathbbox

$m currentmatrix aload pop

}bd

/popgstate

{

$m astore setmatrix

2 index sub exch

3 index sub exch

rC

array astore exch setdash

setlinejoin

setlinecap

lw

popcolor

np :M

}bd

/bu

{

pushgstate

gR

pushgstate

2state?

{

gR

pushgstate

}if

pushstatic

pm restore

mT concat

}bd

/bn

{

/pm save store

popstatic

popgstate

gS

popgstate

2state?

{

gS

popgstate

}if

}bd

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

%%EndFile

%%BeginFile: adobe_psp_basic_text

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

/S/show ld

/A{

0.0 exch ashow

}bd

/R{

0.0 exch 32 exch widthshow

}bd

/W{

0.0 3 1 roll widthshow

}bd

/J{

0.0 32 4 2 roll 0.0 exch awidthshow

}bd

/V{

0.0 4 1 roll 0.0 exch awidthshow

}bd

/fcflg true def

/fc{

fcflg{

vmstatus exch sub 50000 lt{

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

}if pop

}if

}bd

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

/:ff{$f :mf}bd

/MacEncoding StandardEncoding 256 array copy def

MacEncoding 39/quotesingle put

MacEncoding 96/grave put

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

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

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

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

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

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

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

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

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

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

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

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

/daggerdbl/periodcentered/quotesinglbase/quotedblbase/perthousand

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

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

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

MacEncoding 128 128 getinterval astore pop

level2 startnoload

/copyfontdict

{

findfont dup length dict

begin

{

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

}forall

}bd

level2 endnoload level2 not startnoload

/copyfontdict

{

findfont dup length dict

copy

begin

}bd

level2 not endnoload

md/fontname known not{

/fontname/customfont def

}if

/Encoding Z

/:mre

{

copyfontdict

/Encoding MacEncoding def

fontname currentdict

end

definefont :ff def

}bd

/:bsr

{

copyfontdict

/Encoding Encoding 256 array copy def

Encoding dup

}bd

/pd{put dup}bd

/:esr

{

pop pop

fontname currentdict

end

definefont :ff def

}bd

/scf

{

scalefont def

}bd

/scf-non

{

$m scale :mf setfont

}bd

/ps Z

/fz{/ps xs}bd

/sf/setfont ld

/cF/currentfont ld

/mbf

{

/makeblendedfont where

{

pop

makeblendedfont

/ABlend exch definefont

}{

pop

}ifelse

def

}def

%%EndFile

/currentpacking where {pop sc_oldpacking setpacking}if

end		% md

%%EndProlog

%%BeginSetup

md begin

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

/sD 16 dict def

%%IncludeFont: Times-Roman

/f0_1/Times-Roman :mre

/f0_40 f0_1 40 scf

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

%PostScript Hack by Mike Brors 12/7/90

/DisableNextSetRGBColor

	{

	userdict begin

	/setrgbcolor 

		{

		pop

		pop

		pop

		userdict begin

		/setrgbcolor systemdict /setrgbcolor get def

		end

		} def

	end

} bind def

/bcarray where {

	pop

	bcarray 2 {

		/da 4 ps div def

		df setfont gsave cs wi

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

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

		gray

		{ gl}

		{1 setgray}ifelse

		da 2. div dup moveto show

	}bind put

} if

%

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

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

	transform

	0.25 sub round 0.25 add exch

	0.25 sub round 0.25 add exch

	itransform

} bind def

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

	stp  moveto

} bind def

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

	stp lineto

} bind def

%%EndSetup

%%Page: 1 1

%%BeginPageSetup

initializepage

%%EndPageSetup

gS 0 0 2152 3124 rC

0 0 :M

.25 0 translate

/DrawObject_save_matrix_0 matrix currentmatrix def

0 0 2152 2912 rC

-40 -12 :M

DrawObject_save_matrix_0 setmatrix

/DrawObject_save_matrix_0 matrix currentmatrix def

-40 -12 :M

/DrawObject_save_matrix_1 matrix currentmatrix def

0 0 2152 2911 rC

-40 -12 :M

/DrawObject_save_matrix_2 matrix currentmatrix def

-40 -12 :M

DrawObject_save_matrix_2 setmatrix

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

558 556 208 48 rC

558 556 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

gR

gS 553 520 218 84 rC

558 592 :M

f0_40 sf

-.055(Pure Isabelle)A

gR

gS 0 0 2152 2912 rC

4 lw

518 528 806 636 32 @s

168 24 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

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

426 418 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

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

786 526 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

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

588 418 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

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

714 526 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

376 364 92 48 rC

376 364 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

gR

gS 371 328 102 84 rC

376 400 :M

f0_40 sf

-.286(IFOL)A

gR

gS 556 364 76 48 rC

556 364 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

gR

gS 551 328 86 84 rC

556 400 :M

f0_40 sf

-.273(CTT)A

gR

gS 700 364 84 48 rC

700 364 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

gR

gS 695 328 94 84 rC

700 400 :M

f0_40 sf

-.094(HOL)A

gR

gS 880 364 56 48 rC

880 364 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

gR

gS 875 328 66 84 rC

880 400 :M

f0_40 sf

-.311(LK)A

gR

gS 0 0 2152 2912 rC

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

4 lw

912 357 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

320 94 :M

/DrawObject_save_matrix_2 matrix currentmatrix def

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

336 148 :M

DrawObject_save_matrix_2 setmatrix

/DrawObject_save_matrix_2 matrix currentmatrix def

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

426 220 :M

DrawObject_save_matrix_2 setmatrix

/DrawObject_save_matrix_2 matrix currentmatrix def

320 94 48 48 rC

320 94 :M

DrawObject_save_matrix_2 setmatrix

/DrawObject_save_matrix_2 matrix currentmatrix def

gR

gS 315 58 58 84 rC

320 130 :M

f0_40 sf

-.67(ZF)A

gR

gS 448 94 76 48 rC

448 94 :M

DrawObject_save_matrix_2 setmatrix

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

gR

gS 443 58 86 84 rC

448 130 :M

f0_40 sf

-.175(LCF)A

gR

gS 860 178 116 96 rC

gR

gS 855 142 126 132 rC

860 214 :M

f0_40 sf

-.106(Modal)A

975 262 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

860 262 :M

-.077(  logics)A

gR

gS 0 0 2152 2912 rC

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

4 lw

408 356 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

376 228 76 48 rC

376 228 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

gR

gS 371 192 86 84 rC

376 264 :M

f0_40 sf

-.273(FOL)A

gR

gS 680 230 132 48 rC

680 230 :M

DrawObject_save_matrix_1 setmatrix

/DrawObject_save_matrix_1 matrix currentmatrix def

gR

gS 675 194 142 84 rC

680 266 :M

f0_40 sf

-.026(HOLCF)A

gR

gS 0 0 2152 2912 rC

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

4 lw

744 357 :M

DrawObject_save_matrix_1 setmatrix

DrawObject_save_matrix_0 setmatrix

endp

%%Trailer

end		% md

%%EOF