doc-src/Isa-logics.eps

Removed an old bug which made some simultaneous instantiations fail if they
were given in the "wrong" order.

Rewrote sign/infer_types.

Fixed some comments.

%!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