# HG changeset patch # User wenzelm # Date 789045266 -3600 # Node ID 5716e174b591461bf104427d64e862fb51752571 # Parent 1aa6b351ca349e7b650a01d1cb901d1c6b5fdd40 added; diff -r 1aa6b351ca34 -r 5716e174b591 doc-src/Isa-logics.eps --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Isa-logics.eps Mon Jan 02 12:14:26 1995 +0100 @@ -0,0 +1,575 @@ +%!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