1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Isa-logics.eps Mon Jan 02 12:14:26 1995 +0100
1.3 @@ -0,0 +1,575 @@
1.4 +%!PS-Adobe-3.0 EPSF-3.0
1.5 +%%BoundingBox: 116 648 289 789
1.6 +%%Title: (set-I figures-Layer#1)
1.7 +%%Creator: (MacDraw II 1.1: LaserWriter 8 8.1.1)
1.8 +%%CreationDate: (11:19 am Sunday, January 9, 1994)
1.9 +%%For: ()
1.10 +%%Pages: 1
1.11 +%%DocumentFonts: Helvetica
1.12 +%%DocumentNeededFonts: Helvetica
1.13 +%%DocumentSuppliedFonts:
1.14 +%%DocumentData: Clean7Bit
1.15 +%%PageOrder: Ascend
1.16 +%%Orientation: Portrait
1.17 +%ADO_PaperArea: -129 -117 3379 2362
1.18 +%ADO_ImageableArea: 0 0 3254 2242
1.19 +%%EndComments
1.20 +/md 150 dict def md begin
1.21 +/currentpacking where {pop /sc_oldpacking currentpacking def true setpacking}if
1.22 +%%BeginFile: adobe_psp_basic
1.23 +%%Copyright: Copyright 1990-1993 Adobe Systems Incorporated. All Rights Reserved.
1.24 +/bd{bind def}bind def
1.25 +/xdf{exch def}bd
1.26 +/xs{exch store}bd
1.27 +/ld{load def}bd
1.28 +/Z{0 def}bd
1.29 +/T/true
1.30 +/F/false
1.31 +/:L/lineto
1.32 +/lw/setlinewidth
1.33 +/:M/moveto
1.34 +/rl/rlineto
1.35 +/rm/rmoveto
1.36 +/:C/curveto
1.37 +/:T/translate
1.38 +/:K/closepath
1.39 +/:mf/makefont
1.40 +/gS/gsave
1.41 +/gR/grestore
1.42 +/np/newpath
1.43 +14{ld}repeat
1.44 +/$m matrix def
1.45 +/av 81 def
1.46 +/por true def
1.47 +/normland false def
1.48 +/psb-nosave{}bd
1.49 +/pse-nosave{}bd
1.50 +/us Z
1.51 +/psb{/us save store}bd
1.52 +/pse{us restore}bd
1.53 +/level2
1.54 +/languagelevel where
1.55 +{
1.56 +pop languagelevel 2 ge
1.57 +}{
1.58 +false
1.59 +}ifelse
1.60 +def
1.61 +/featurecleanup
1.62 +{
1.63 +stopped
1.64 +cleartomark
1.65 +countdictstack exch sub dup 0 gt
1.66 +{
1.67 +{end}repeat
1.68 +}{
1.69 +pop
1.70 +}ifelse
1.71 +}bd
1.72 +/noload Z
1.73 +/startnoload
1.74 +{
1.75 +{/noload save store}if
1.76 +}bd
1.77 +/endnoload
1.78 +{
1.79 +{noload restore}if
1.80 +}bd
1.81 +level2 startnoload
1.82 +/setjob
1.83 +{
1.84 +statusdict/jobname 3 -1 roll put
1.85 +}bd
1.86 +/setcopies
1.87 +{
1.88 +userdict/#copies 3 -1 roll put
1.89 +}bd
1.90 +level2 endnoload level2 not startnoload
1.91 +/setjob
1.92 +{
1.93 +1 dict begin/JobName xdf currentdict end setuserparams
1.94 +}bd
1.95 +/setcopies
1.96 +{
1.97 +1 dict begin/NumCopies xdf currentdict end setpagedevice
1.98 +}bd
1.99 +level2 not endnoload
1.100 +/pm Z
1.101 +/mT Z
1.102 +/sD Z
1.103 +/realshowpage Z
1.104 +/initializepage
1.105 +{
1.106 +/pm save store mT concat
1.107 +}bd
1.108 +/endp
1.109 +{
1.110 +pm restore showpage
1.111 +}def
1.112 +/$c/DeviceRGB def
1.113 +/rectclip where
1.114 +{
1.115 +pop/rC/rectclip ld
1.116 +}{
1.117 +/rC
1.118 +{
1.119 +np 4 2 roll
1.120 +:M
1.121 +1 index 0 rl
1.122 +0 exch rl
1.123 +neg 0 rl
1.124 +:K
1.125 +clip np
1.126 +}bd
1.127 +}ifelse
1.128 +/rectfill where
1.129 +{
1.130 +pop/rF/rectfill ld
1.131 +}{
1.132 +/rF
1.133 +{
1.134 +gS
1.135 +np
1.136 +4 2 roll
1.137 +:M
1.138 +1 index 0 rl
1.139 +0 exch rl
1.140 +neg 0 rl
1.141 +fill
1.142 +gR
1.143 +}bd
1.144 +}ifelse
1.145 +/rectstroke where
1.146 +{
1.147 +pop/rS/rectstroke ld
1.148 +}{
1.149 +/rS
1.150 +{
1.151 +gS
1.152 +np
1.153 +4 2 roll
1.154 +:M
1.155 +1 index 0 rl
1.156 +0 exch rl
1.157 +neg 0 rl
1.158 +:K
1.159 +stroke
1.160 +gR
1.161 +}bd
1.162 +}ifelse
1.163 +%%EndFile
1.164 +%%BeginFile: adobe_psp_colorspace_level1
1.165 +%%Copyright: Copyright 1991-1993 Adobe Systems Incorporated. All Rights Reserved.
1.166 +/G/setgray ld
1.167 +/:F/setrgbcolor ld
1.168 +%%EndFile
1.169 +%%BeginFile: adobe_psp_uniform_graphics
1.170 +%%Copyright: Copyright 1990-1993 Adobe Systems Incorporated. All Rights Reserved.
1.171 +/@a
1.172 +{
1.173 +np :M 0 rl :L 0 exch rl 0 rl :L fill
1.174 +}bd
1.175 +/@b
1.176 +{
1.177 +np :M 0 rl 0 exch rl :L 0 rl 0 exch rl fill
1.178 +}bd
1.179 +/arct where
1.180 +{
1.181 +pop
1.182 +}{
1.183 +/arct
1.184 +{
1.185 +arcto pop pop pop pop
1.186 +}bd
1.187 +}ifelse
1.188 +/x1 Z
1.189 +/x2 Z
1.190 +/y1 Z
1.191 +/y2 Z
1.192 +/rad Z
1.193 +/@q
1.194 +{
1.195 +/rad xs
1.196 +/y2 xs
1.197 +/x2 xs
1.198 +/y1 xs
1.199 +/x1 xs
1.200 +np
1.201 +x2 x1 add 2 div y1 :M
1.202 +x2 y1 x2 y2 rad arct
1.203 +x2 y2 x1 y2 rad arct
1.204 +x1 y2 x1 y1 rad arct
1.205 +x1 y1 x2 y1 rad arct
1.206 +fill
1.207 +}bd
1.208 +/@s
1.209 +{
1.210 +/rad xs
1.211 +/y2 xs
1.212 +/x2 xs
1.213 +/y1 xs
1.214 +/x1 xs
1.215 +np
1.216 +x2 x1 add 2 div y1 :M
1.217 +x2 y1 x2 y2 rad arct
1.218 +x2 y2 x1 y2 rad arct
1.219 +x1 y2 x1 y1 rad arct
1.220 +x1 y1 x2 y1 rad arct
1.221 +:K
1.222 +stroke
1.223 +}bd
1.224 +/@i
1.225 +{
1.226 +np 0 360 arc fill
1.227 +}bd
1.228 +/@j
1.229 +{
1.230 +gS
1.231 +np
1.232 +:T
1.233 +scale
1.234 +0 0 .5 0 360 arc
1.235 +fill
1.236 +gR
1.237 +}bd
1.238 +/@e
1.239 +{
1.240 +np
1.241 +0 360 arc
1.242 +:K
1.243 +stroke
1.244 +}bd
1.245 +/@f
1.246 +{
1.247 +np
1.248 +$m currentmatrix
1.249 +pop
1.250 +:T
1.251 +scale
1.252 +0 0 .5 0 360 arc
1.253 +:K
1.254 +$m setmatrix
1.255 +stroke
1.256 +}bd
1.257 +/@k
1.258 +{
1.259 +gS
1.260 +np
1.261 +:T
1.262 +0 0 :M
1.263 +0 0 5 2 roll
1.264 +arc fill
1.265 +gR
1.266 +}bd
1.267 +/@l
1.268 +{
1.269 +gS
1.270 +np
1.271 +:T
1.272 +0 0 :M
1.273 +scale
1.274 +0 0 .5 5 -2 roll arc
1.275 +fill
1.276 +gR
1.277 +}bd
1.278 +/@m
1.279 +{
1.280 +np
1.281 +arc
1.282 +stroke
1.283 +}bd
1.284 +/@n
1.285 +{
1.286 +np
1.287 +$m currentmatrix
1.288 +pop
1.289 +:T
1.290 +scale
1.291 +0 0 .5 5 -2 roll arc
1.292 +$m setmatrix
1.293 +stroke
1.294 +}bd
1.295 +%%EndFile
1.296 +%%BeginFile: adobe_psp_customps
1.297 +%%Copyright: Copyright 1990-1993 Adobe Systems Incorporated. All Rights Reserved.
1.298 +/$t Z
1.299 +/$p Z
1.300 +/$s Z
1.301 +/$o 1. def
1.302 +/2state? false def
1.303 +/ps Z
1.304 +level2 startnoload
1.305 +/pushcolor/currentrgbcolor ld
1.306 +/popcolor/setrgbcolor ld
1.307 +/setcmykcolor where
1.308 +{
1.309 +pop/currentcmykcolor where
1.310 +{
1.311 +pop/pushcolor/currentcmykcolor ld
1.312 +/popcolor/setcmykcolor ld
1.313 +}if
1.314 +}if
1.315 +level2 endnoload level2 not startnoload
1.316 +/pushcolor
1.317 +{
1.318 +currentcolorspace $c eq
1.319 +{
1.320 +currentcolor currentcolorspace true
1.321 +}{
1.322 +currentcmykcolor false
1.323 +}ifelse
1.324 +}bd
1.325 +/popcolor
1.326 +{
1.327 +{
1.328 +setcolorspace setcolor
1.329 +}{
1.330 +setcmykcolor
1.331 +}ifelse
1.332 +}bd
1.333 +level2 not endnoload
1.334 +/pushstatic
1.335 +{
1.336 +ps
1.337 +2state?
1.338 +$o
1.339 +$t
1.340 +$p
1.341 +$s
1.342 +}bd
1.343 +/popstatic
1.344 +{
1.345 +/$s xs
1.346 +/$p xs
1.347 +/$t xs
1.348 +/$o xs
1.349 +/2state? xs
1.350 +/ps xs
1.351 +}bd
1.352 +/pushgstate
1.353 +{
1.354 +save errordict/nocurrentpoint{pop 0 0}put
1.355 +currentpoint
1.356 +3 -1 roll restore
1.357 +pushcolor
1.358 +currentlinewidth
1.359 +currentlinecap
1.360 +currentlinejoin
1.361 +currentdash exch aload length
1.362 +np clippath pathbbox
1.363 +$m currentmatrix aload pop
1.364 +}bd
1.365 +/popgstate
1.366 +{
1.367 +$m astore setmatrix
1.368 +2 index sub exch
1.369 +3 index sub exch
1.370 +rC
1.371 +array astore exch setdash
1.372 +setlinejoin
1.373 +setlinecap
1.374 +lw
1.375 +popcolor
1.376 +np :M
1.377 +}bd
1.378 +/bu
1.379 +{
1.380 +pushgstate
1.381 +gR
1.382 +pushgstate
1.383 +2state?
1.384 +{
1.385 +gR
1.386 +pushgstate
1.387 +}if
1.388 +pushstatic
1.389 +pm restore
1.390 +mT concat
1.391 +}bd
1.392 +/bn
1.393 +{
1.394 +/pm save store
1.395 +popstatic
1.396 +popgstate
1.397 +gS
1.398 +popgstate
1.399 +2state?
1.400 +{
1.401 +gS
1.402 +popgstate
1.403 +}if
1.404 +}bd
1.405 +/cpat{pop 64 div G 8{pop}repeat}bd
1.406 +%%EndFile
1.407 +%%BeginFile: adobe_psp_basic_text
1.408 +%%Copyright: Copyright 1990-1993 Adobe Systems Incorporated. All Rights Reserved.
1.409 +/S/show ld
1.410 +/A{
1.411 +0.0 exch ashow
1.412 +}bd
1.413 +/R{
1.414 +0.0 exch 32 exch widthshow
1.415 +}bd
1.416 +/W{
1.417 +0.0 3 1 roll widthshow
1.418 +}bd
1.419 +/J{
1.420 +0.0 32 4 2 roll 0.0 exch awidthshow
1.421 +}bd
1.422 +/V{
1.423 +0.0 4 1 roll 0.0 exch awidthshow
1.424 +}bd
1.425 +/fcflg true def
1.426 +/fc{
1.427 +fcflg{
1.428 +vmstatus exch sub 50000 lt{
1.429 +(%%[ Warning: Running out of memory ]%%\r)print flush/fcflg false store
1.430 +}if pop
1.431 +}if
1.432 +}bd
1.433 +/$f[1 0 0 -1 0 0]def
1.434 +/:ff{$f :mf}bd
1.435 +/MacEncoding StandardEncoding 256 array copy def
1.436 +MacEncoding 39/quotesingle put
1.437 +MacEncoding 96/grave put
1.438 +/Adieresis/Aring/Ccedilla/Eacute/Ntilde/Odieresis/Udieresis/aacute
1.439 +/agrave/acircumflex/adieresis/atilde/aring/ccedilla/eacute/egrave
1.440 +/ecircumflex/edieresis/iacute/igrave/icircumflex/idieresis/ntilde/oacute
1.441 +/ograve/ocircumflex/odieresis/otilde/uacute/ugrave/ucircumflex/udieresis
1.442 +/dagger/degree/cent/sterling/section/bullet/paragraph/germandbls
1.443 +/registered/copyright/trademark/acute/dieresis/notequal/AE/Oslash
1.444 +/infinity/plusminus/lessequal/greaterequal/yen/mu/partialdiff/summation
1.445 +/product/pi/integral/ordfeminine/ordmasculine/Omega/ae/oslash
1.446 +/questiondown/exclamdown/logicalnot/radical/florin/approxequal/Delta/guillemotleft
1.447 +/guillemotright/ellipsis/space/Agrave/Atilde/Otilde/OE/oe
1.448 +/endash/emdash/quotedblleft/quotedblright/quoteleft/quoteright/divide/lozenge
1.449 +/ydieresis/Ydieresis/fraction/currency/guilsinglleft/guilsinglright/fi/fl
1.450 +/daggerdbl/periodcentered/quotesinglbase/quotedblbase/perthousand
1.451 +/Acircumflex/Ecircumflex/Aacute/Edieresis/Egrave/Iacute/Icircumflex/Idieresis/Igrave
1.452 +/Oacute/Ocircumflex/apple/Ograve/Uacute/Ucircumflex/Ugrave/dotlessi/circumflex/tilde
1.453 +/macron/breve/dotaccent/ring/cedilla/hungarumlaut/ogonek/caron
1.454 +MacEncoding 128 128 getinterval astore pop
1.455 +level2 startnoload
1.456 +/copyfontdict
1.457 +{
1.458 +findfont dup length dict
1.459 +begin
1.460 +{
1.461 +1 index/FID ne{def}{pop pop}ifelse
1.462 +}forall
1.463 +}bd
1.464 +level2 endnoload level2 not startnoload
1.465 +/copyfontdict
1.466 +{
1.467 +findfont dup length dict
1.468 +copy
1.469 +begin
1.470 +}bd
1.471 +level2 not endnoload
1.472 +md/fontname known not{
1.473 +/fontname/customfont def
1.474 +}if
1.475 +/Encoding Z
1.476 +/:mre
1.477 +{
1.478 +copyfontdict
1.479 +/Encoding MacEncoding def
1.480 +fontname currentdict
1.481 +end
1.482 +definefont :ff def
1.483 +}bd
1.484 +/:bsr
1.485 +{
1.486 +copyfontdict
1.487 +/Encoding Encoding 256 array copy def
1.488 +Encoding dup
1.489 +}bd
1.490 +/pd{put dup}bd
1.491 +/:esr
1.492 +{
1.493 +pop pop
1.494 +fontname currentdict
1.495 +end
1.496 +definefont :ff def
1.497 +}bd
1.498 +/scf
1.499 +{
1.500 +scalefont def
1.501 +}bd
1.502 +/scf-non
1.503 +{
1.504 +$m scale :mf setfont
1.505 +}bd
1.506 +/ps Z
1.507 +/fz{/ps xs}bd
1.508 +/sf/setfont ld
1.509 +/cF/currentfont ld
1.510 +/mbf
1.511 +{
1.512 +/makeblendedfont where
1.513 +{
1.514 +pop
1.515 +makeblendedfont
1.516 +/ABlend exch definefont
1.517 +}{
1.518 +pop
1.519 +}ifelse
1.520 +def
1.521 +}def
1.522 +%%EndFile
1.523 +/currentpacking where {pop sc_oldpacking setpacking}if
1.524 +end % md
1.525 +%%EndProlog
1.526 +%%BeginSetup
1.527 +md begin
1.528 +/pT[1 0 0 -1 28.079 810.927]def/mT[.24 0 0 -.24 28.079 810.927]def
1.529 +/sD 16 dict def
1.530 +%%IncludeFont: Helvetica
1.531 +/f0_1/Helvetica :mre
1.532 +/f0_42 f0_1 42 scf
1.533 +/Courier findfont[10 0 0 -10 0 0]:mf setfont
1.534 +%%EndSetup
1.535 +%%Page: 1 1
1.536 +%%BeginPageSetup
1.537 +initializepage
1.538 +%%EndPageSetup
1.539 +gS 0 0 2242 3254 rC
1.540 +0 0 :M
1.541 +0 setlinecap
1.542 +currentscreen
1.543 +3 1 roll pop pop 60 45 3 -1 roll setscreen
1.544 +601 638 :M
1.545 +f0_42 sf
1.546 +-.005(Pure Isabelle)A
1.547 +4 lw
1.548 +563 563 900 675 35.5 @s
1.549 +486 452 -4 4 602 561 4 486 448 @a
1.550 +-4 -4 865 565 4 4 973 448 @b
1.551 +654 452 -4 4 677 561 4 654 448 @a
1.552 +-4 -4 790 565 4 4 804 448 @b
1.553 +434 434 :M
1.554 +-.447(IFOL)A
1.555 +622 434 :M
1.556 +-.816(CTT)A
1.557 +772 434 :M
1.558 +-.669(HOL)A
1.559 +959 434 :M
1.560 +-1.362(LK)A
1.561 +-4 -4 996 377 4 4 992 298 @b
1.562 +392 152 -4 4 452 223 4 392 148 @a
1.563 +-4 -4 490 227 4 4 542 148 @b
1.564 +376 134 :M
1.565 +-1.311(ZF)A
1.566 +509 134 :M
1.567 +-.662(LCF)A
1.568 +939 225 :M
1.569 +-.335(Modal)A
1.570 +939 279 :M
1.571 +-.268(logics)A
1.572 +-4 -4 471 377 4 4 467 298 @b
1.573 +434 284 :M
1.574 +-.836(FOL)A
1.575 +endp
1.576 +%%Trailer
1.577 +end % md
1.578 +%%EOF