# 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