%!PS-Adobe-3.0 EPSF-3.0

%%BoundingBox: 116 648 289 789

%%Title: (set-I figures-Layer#1)

%%Creator: (MacDraw II 1.1: LaserWriter 8 8.1.1)

%%CreationDate: (11:19 am Sunday, January 9, 1994)

%%For: ()

%%Pages: 1

%%DocumentFonts: Helvetica

%%DocumentNeededFonts: Helvetica

%%DocumentSuppliedFonts:

%%DocumentData: Clean7Bit

%%PageOrder: Ascend

%%Orientation: Portrait

%ADO_PaperArea: -129 -117 3379 2362

%ADO_ImageableArea: 0 0 3254 2242

%%EndComments

/md 150 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.079 810.927]def/mT[.24 0 0 -.24 28.079 810.927]def

/sD 16 dict def

%%IncludeFont: Helvetica

/f0_1/Helvetica :mre

/f0_42 f0_1 42 scf

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

%%EndSetup

%%Page: 1 1

%%BeginPageSetup

initializepage

%%EndPageSetup

gS 0 0 2242 3254 rC

0 0 :M

0 setlinecap

currentscreen

3 1 roll pop pop 60 45 3 -1 roll setscreen

601 638 :M

f0_42 sf

-.005(Pure Isabelle)A

4 lw

563 563 900 675 35.5 @s

486 452 -4 4 602 561 4 486 448 @a

-4 -4 865 565 4 4 973 448 @b

654 452 -4 4 677 561 4 654 448 @a

-4 -4 790 565 4 4 804 448 @b

434 434 :M

-.447(IFOL)A

622 434 :M

-.816(CTT)A

772 434 :M

-.669(HOL)A

959 434 :M

-1.362(LK)A

-4 -4 996 377 4 4 992 298 @b

392 152 -4 4 452 223 4 392 148 @a

-4 -4 490 227 4 4 542 148 @b

376 134 :M

-1.311(ZF)A

509 134 :M

-.662(LCF)A

939 225 :M

-.335(Modal)A

939 279 :M

-.268(logics)A

-4 -4 471 377 4 4 467 298 @b

434 284 :M

-.836(FOL)A

endp

%%Trailer

end		% md

%%EOF