diff -r 57165d7271b5 -r 6ef3742b6153 doc-src/gfx/Isa-logics.eps
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/gfx/Isa-logics.eps	Wed Aug 26 16:33:29 1998 +0200
@@ -0,0 +1,753 @@
+%!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