--- a/doc-src/Isa-logics.eps Mon Aug 24 21:09:59 1998 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,753 +0,0 @@
-%!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