From 47992200e628aa4c403496bcbe9116b0a4f8cdcd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 18 Jan 2006 12:09:29 +0000 Subject: [PATCH] libraries.ps no longer in synch. --- helm/papers/matita/libraries.ps | 1657 ------------------------------- helm/papers/matita/matita2.tex | 8 - 2 files changed, 1665 deletions(-) delete mode 100644 helm/papers/matita/libraries.ps diff --git a/helm/papers/matita/libraries.ps b/helm/papers/matita/libraries.ps deleted file mode 100644 index 1d47f4b35..000000000 --- a/helm/papers/matita/libraries.ps +++ /dev/null @@ -1,1657 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: dot version 2.2.1 (Fri Sep 30 13:22:44 UTC 2005) -%%For: (sacerdot) Claudio Sacerdoti Coen,,, -%%Title: G -%%Pages: (atend) -%%BoundingBox: 35 35 606 873 -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval - -EncodingVector - dup 306 /AE - dup 301 /Aacute - dup 302 /Acircumflex - dup 304 /Adieresis - dup 300 /Agrave - dup 305 /Aring - dup 303 /Atilde - dup 307 /Ccedilla - dup 311 /Eacute - dup 312 /Ecircumflex - dup 313 /Edieresis - dup 310 /Egrave - dup 315 /Iacute - dup 316 /Icircumflex - dup 317 /Idieresis - dup 314 /Igrave - dup 334 /Udieresis - dup 335 /Yacute - dup 376 /thorn - dup 337 /germandbls - dup 341 /aacute - dup 342 /acircumflex - dup 344 /adieresis - dup 346 /ae - dup 340 /agrave - dup 345 /aring - dup 347 /ccedilla - dup 351 /eacute - dup 352 /ecircumflex - dup 353 /edieresis - dup 350 /egrave - dup 355 /iacute - dup 356 /icircumflex - dup 357 /idieresis - dup 354 /igrave - dup 360 /dcroat - dup 361 /ntilde - dup 363 /oacute - dup 364 /ocircumflex - dup 366 /odieresis - dup 362 /ograve - dup 365 /otilde - dup 370 /oslash - dup 372 /uacute - dup 373 /ucircumflex - dup 374 /udieresis - dup 371 /ugrave - dup 375 /yacute - dup 377 /ydieresis - -% Set up ISO Latin 1 character encoding -/starnetISO { - dup dup findfont dup length dict begin - { 1 index /FID ne { def }{ pop pop } ifelse - } forall - /Encoding EncodingVector def - currentdict end definefont -} def -/Times-Roman starnetISO def -/Times-Italic starnetISO def -/Times-Bold starnetISO def -/Times-BoldItalic starnetISO def -/Helvetica starnetISO def -/Helvetica-Oblique starnetISO def -/Helvetica-Bold starnetISO def -/Helvetica-BoldOblique starnetISO def -/Courier starnetISO def -/Courier-Oblique starnetISO def -/Courier-Bold starnetISO def -/Courier-BoldOblique starnetISO def -cleartomark -} bind def - -%%BeginResource: procset graphviz 0 0 -/coord-font-family /Times-Roman def -/default-font-family /Times-Roman def -/coordfont coord-font-family findfont 8 scalefont def - -/InvScaleFactor 1.0 def -/set_scale { - dup 1 exch div /InvScaleFactor exch def - dup scale -} bind def - -% styles -/solid { [] 0 setdash } bind def -/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def -/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def -/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def -/bold { 2 setlinewidth } bind def -/filled { } bind def -/unfilled { } bind def -/rounded { } bind def -/diagonals { } bind def - -% hooks for setting color -/nodecolor { sethsbcolor } bind def -/edgecolor { sethsbcolor } bind def -/graphcolor { sethsbcolor } bind def -/nopcolor {pop pop pop} bind def - -/beginpage { % i j npages - /npages exch def - /j exch def - /i exch def - /str 10 string def - npages 1 gt { - gsave - coordfont setfont - 0 0 moveto - (\() show i str cvs show (,) show j str cvs show (\)) show - grestore - } if -} bind def - -/set_font { - findfont exch - scalefont setfont -} def - -% draw aligned label in bounding box aligned to current point -/alignedtext { % width adj text - /text exch def - /adj exch def - /width exch def - gsave - width 0 gt { - text stringwidth pop adj mul 0 rmoveto - } if - [] 0 setdash - text show - grestore -} def - -/boxprim { % xcorner ycorner xsize ysize - 4 2 roll - moveto - 2 copy - exch 0 rlineto - 0 exch rlineto - pop neg 0 rlineto - closepath -} bind def - -/ellipse_path { - /ry exch def - /rx exch def - /y exch def - /x exch def - matrix currentmatrix - newpath - x y translate - rx ry scale - 0 0 1 0 360 arc - setmatrix -} bind def - -/endpage { showpage } bind def -/showpage { } def - -/layercolorseq - [ % layer color sequence - darkest to lightest - [0 0 0] - [.2 .8 .8] - [.4 .8 .8] - [.6 .8 .8] - [.8 .8 .8] - ] -def - -/layerlen layercolorseq length def - -/setlayer {/maxlayer exch def /curlayer exch def - layercolorseq curlayer 1 sub layerlen mod get - aload pop sethsbcolor - /nodecolor {nopcolor} def - /edgecolor {nopcolor} def - /graphcolor {nopcolor} def -} bind def - -/onlayer { curlayer ne {invis} if } def - -/onlayers { - /myupper exch def - /mylower exch def - curlayer mylower lt - curlayer myupper gt - or - {invis} if -} def - -/curlayer 0 def - -%%EndResource -%%EndProlog -%%BeginSetup -14 default-font-family set_font -1 setmiterlimit -% /arrowlength 10 def -% /arrowwidth 5 def - -% make sure pdfmark is harmless for PS-interpreters other than Distiller -/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse -% make '<<' and '>>' safe on PS Level 1 devices -/languagelevel where {pop languagelevel}{1} ifelse -2 lt { - userdict (<<) cvn ([) cvn load put - userdict (>>) cvn ([) cvn load put -} if - -%%EndSetup -%%Page: 1 1 -%%PageBoundingBox: 36 36 606 873 -%%PageOrientation: Portrait -gsave -35 35 571 838 boxprim clip newpath -36 36 translate -0 0 1 beginpage -0 0 translate 0 rotate -0.000 0.000 0.000 graphcolor -14.00 /Times-Roman set_font - -% DependencyAnalyzer -gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 287 476 moveto -201 476 lineto -201 436 lineto -287 436 lineto -closepath -fill -0.584 0.220 0.933 nodecolor -newpath 287 476 moveto -201 476 lineto -201 436 lineto -287 436 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -209 459 moveto -(Dependency) -[10.08 6.24 6.96 6.24 6.96 6.96 6.24 6.96 6.24 6.96] -xshow -217 443 moveto -(Analyzer) -[10.08 6.96 6.24 3.84 6.96 6.24 6.24 4.56] -xshow -end grestore -end grestore - -% metadata -gsave 10 dict begin -191 380 38 18 ellipse_path -stroke -gsave 10 dict begin -165 375 moveto -(metadata) -[10.8 6.24 3.84 6.24 6.96 6.24 3.84 6.24] -xshow -end grestore -end grestore - -% DependencyAnalyzer -> metadata -newpath 230 436 moveto -223 427 215 416 209 406 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 211 403 moveto -203 397 lineto -206 407 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 211 403 moveto -203 397 lineto -206 407 lineto -closepath -stroke -end grestore - -% Getter -gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 408 324 moveto -354 324 lineto -354 288 lineto -408 288 lineto -closepath -fill -0.584 0.220 0.933 nodecolor -newpath 408 324 moveto -354 324 lineto -354 288 lineto -408 288 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -363 301 moveto -(Getter) -[10.08 6.24 3.84 3.84 6.24 4.56] -xshow -end grestore -end grestore - -% getter -gsave 10 dict begin -275 234 29 18 ellipse_path -stroke -gsave 10 dict begin -259 229 moveto -(getter) -[6.96 6.24 3.84 3.84 6.24 4.56] -xshow -end grestore -end grestore - -% Getter -> getter -newpath 354 288 moveto -339 278 319 264 303 254 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 305 251 moveto -295 248 lineto -301 257 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 305 251 moveto -295 248 lineto -301 257 lineto -closepath -stroke -end grestore - -% Matita -gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 259 836 moveto -205 836 lineto -205 800 lineto -259 800 lineto -closepath -fill -0.584 0.220 0.933 nodecolor -newpath 259 836 moveto -205 836 lineto -205 800 lineto -259 800 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -213 813 moveto -(Matita) -[12.48 6.24 3.84 3.84 3.84 6.24] -xshow -end grestore -end grestore - -% cic_disambiguation -gsave 10 dict begin -313 602 68 18 ellipse_path -stroke -gsave 10 dict begin -258 597 moveto -(cic_disambiguation) -[6.24 3.84 6.24 6.96 6.96 3.84 5.52 6.24 10.8 6.96 3.84 6.96 6.96 6.24 3.84 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Matita -> cic_disambiguation -newpath 259 801 moveto -272 792 286 779 294 764 curveto -316 721 317 664 316 630 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 319 630 moveto -315 620 lineto -313 630 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 319 630 moveto -315 620 lineto -313 630 lineto -closepath -stroke -end grestore - -% grafite_engine -gsave 10 dict begin -232 746 53 18 ellipse_path -stroke -gsave 10 dict begin -191 741 moveto -(grafite_engine) -[6.96 4.56 6.24 4.56 3.84 3.84 6.24 6.96 6.24 6.96 6.96 3.84 6.96 6.24] -xshow -end grestore -end grestore - -% Matita -> grafite_engine -newpath 232 800 moveto -232 792 232 783 232 774 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 236 774 moveto -232 764 lineto -229 774 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 236 774 moveto -232 764 lineto -229 774 lineto -closepath -stroke -end grestore - -% grafite_parser -gsave 10 dict begin -393 746 52 18 ellipse_path -stroke -gsave 10 dict begin -354 741 moveto -(grafite_parser) -[6.96 4.56 6.24 4.56 3.84 3.84 6.24 6.96 6.96 6.24 4.56 5.52 6.24 4.56] -xshow -end grestore -end grestore - -% Matita -> grafite_parser -newpath 259 806 moveto -284 794 322 777 351 764 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 353 767 moveto -361 760 lineto -350 760 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 353 767 moveto -361 760 lineto -350 760 lineto -closepath -stroke -end grestore - -% hgdome -gsave 10 dict begin -36 602 36 18 ellipse_path -stroke -gsave 10 dict begin -12 597 moveto -(hgdome) -[6.96 6.96 6.96 6.96 10.8 6.24] -xshow -end grestore -end grestore - -% Matita -> hgdome -newpath 205 816 moveto -129 801 85 826 38 764 curveto -9 725 19 665 27 630 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 30 631 moveto -30 620 lineto -24 629 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 30 631 moveto -30 620 lineto -24 629 lineto -closepath -stroke -end grestore - -% paramodulation -gsave 10 dict begin -104 746 57 18 ellipse_path -stroke -gsave 10 dict begin -59 741 moveto -(paramodulation) -[6.96 6.24 4.56 6.24 10.8 6.96 6.96 6.96 3.84 6.24 3.84 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Matita -> paramodulation -newpath 205 803 moveto -186 793 161 778 141 767 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 142 764 moveto -132 762 lineto -139 770 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 142 764 moveto -132 762 lineto -139 770 lineto -closepath -stroke -end grestore - -% ProofChecker -gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 309 400 moveto -247 400 lineto -247 360 lineto -309 360 lineto -closepath -fill -0.584 0.220 0.933 nodecolor -newpath 309 400 moveto -247 400 lineto -247 360 lineto -309 360 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -262 383 moveto -(Proof) -[7.68 4.56 6.96 6.96 4.56] -xshow -254 367 moveto -(Checker) -[9.36 6.96 6.24 6.24 6.96 6.24 4.56] -xshow -end grestore -end grestore - -% cic_proof_checking -gsave 10 dict begin -268 306 68 18 ellipse_path -stroke -gsave 10 dict begin -212 301 moveto -(cic_proof_checking) -[6.24 3.84 6.24 6.96 6.96 4.56 6.96 6.96 4.56 6.96 6.24 6.96 6.24 6.24 6.96 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% ProofChecker -> cic_proof_checking -newpath 275 360 moveto -274 352 273 343 272 334 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 275 333 moveto -270 324 lineto -269 334 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 275 333 moveto -270 324 lineto -269 334 lineto -closepath -stroke -end grestore - -% Uwobo -gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 489 692 moveto -431 692 lineto -431 656 lineto -489 656 lineto -closepath -fill -0.584 0.220 0.933 nodecolor -newpath 489 692 moveto -431 692 lineto -431 656 lineto -489 656 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -438 669 moveto -(Uwobo) -[10.08 10.08 6.96 6.96 6.96] -xshow -end grestore -end grestore - -% content_pres -gsave 10 dict begin -454 602 49 18 ellipse_path -stroke -gsave 10 dict begin -418 597 moveto -(content_pres) -[6.24 6.96 6.96 3.84 6.24 6.96 3.84 6.96 6.96 4.56 6.24 5.52] -xshow -end grestore -end grestore - -% Uwobo -> content_pres -newpath 458 656 moveto -457 648 457 639 456 630 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 460 630 moveto -456 620 lineto -453 630 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 460 630 moveto -456 620 lineto -453 630 lineto -closepath -stroke -end grestore - -% Whelp -gsave 10 dict begin -filled -0.584 0.220 0.933 nodecolor -0.584 0.220 0.933 nodecolor -newpath 420 836 moveto -366 836 lineto -366 800 lineto -420 800 lineto -closepath -fill -0.584 0.220 0.933 nodecolor -newpath 420 836 moveto -366 836 lineto -366 800 lineto -420 800 lineto -closepath -stroke -gsave 10 dict begin -0.000 0.000 0.000 nodecolor -373 813 moveto -(Whelp) -[13.2 6.96 6.24 3.84 6.96] -xshow -end grestore -end grestore - -% Whelp -> grafite_parser -newpath 393 800 moveto -393 792 393 783 393 774 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 397 774 moveto -393 764 lineto -390 774 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 397 774 moveto -393 764 lineto -390 774 lineto -closepath -stroke -end grestore - -% cic -gsave 10 dict begin -172 234 27 18 ellipse_path -stroke -gsave 10 dict begin -163 229 moveto -(cic) -[6.24 3.84 6.24] -xshow -end grestore -end grestore - -% metadata -> cic -newpath 189 362 moveto -185 337 179 292 175 262 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 178 262 moveto -174 252 lineto -172 262 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 178 262 moveto -174 252 lineto -172 262 lineto -closepath -stroke -end grestore - -% hmysql -gsave 10 dict begin -401 234 34 18 ellipse_path -stroke -gsave 10 dict begin -379 229 moveto -(hmysql) -[6.96 10.8 6.96 5.52 6.96 3.84] -xshow -end grestore -end grestore - -% metadata -> hmysql -newpath 218 367 moveto -225 364 232 362 238 360 curveto -316 335 365 386 417 324 curveto -431 306 425 280 416 261 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 419 259 moveto -411 252 lineto -413 262 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 419 259 moveto -411 252 lineto -413 262 lineto -closepath -stroke -end grestore - -% urimanager -gsave 10 dict begin -181 162 45 18 ellipse_path -stroke -gsave 10 dict begin -148 157 moveto -(urimanager) -[6.96 4.56 3.84 10.8 6.24 6.96 6.24 6.96 6.24 4.56] -xshow -end grestore -end grestore - -% getter -> urimanager -newpath 256 220 moveto -242 210 225 196 210 184 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 212 181 moveto -202 178 lineto -208 187 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 212 181 moveto -202 178 lineto -208 187 lineto -closepath -stroke -end grestore - -% registry -gsave 10 dict begin -359 162 35 18 ellipse_path -stroke -gsave 10 dict begin -337 157 moveto -(registry) -[4.56 6.24 6.96 3.84 5.52 3.84 4.56 6.96] -xshow -end grestore -end grestore - -% getter -> registry -newpath 292 219 moveto -304 209 319 196 333 185 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 336 187 moveto -341 178 lineto -331 182 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 336 187 moveto -341 178 lineto -331 182 lineto -closepath -stroke -end grestore - -% logger -gsave 10 dict begin -275 162 31 18 ellipse_path -stroke -gsave 10 dict begin -257 157 moveto -(logger) -[3.84 6.96 6.96 6.96 6.24 4.56] -xshow -end grestore -end grestore - -% getter -> logger -newpath 275 216 moveto -275 208 275 199 275 190 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 279 190 moveto -275 180 lineto -272 190 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 279 190 moveto -275 180 lineto -272 190 lineto -closepath -stroke -end grestore - -% cic_unification -gsave 10 dict begin -286 530 55 18 ellipse_path -stroke -gsave 10 dict begin -244 525 moveto -(cic_unification) -[6.24 3.84 6.24 6.96 6.96 6.96 3.84 4.56 3.84 6.24 6.24 3.84 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% cic_disambiguation -> cic_unification -newpath 306 584 moveto -303 576 300 566 296 558 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 299 557 moveto -293 548 lineto -293 559 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 299 557 moveto -293 548 lineto -293 559 lineto -closepath -stroke -end grestore - -% acic_content -gsave 10 dict begin -407 530 48 18 ellipse_path -stroke -gsave 10 dict begin -371 525 moveto -(acic_content) -[6.24 6.24 3.84 6.24 6.96 6.24 6.96 6.96 3.84 6.24 6.96 3.84] -xshow -end grestore -end grestore - -% cic_disambiguation -> acic_content -newpath 335 585 moveto -347 575 364 563 378 552 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 380 555 moveto -386 546 lineto -376 549 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 380 555 moveto -386 546 lineto -376 549 lineto -closepath -stroke -end grestore - -% whelp -gsave 10 dict begin -183 530 30 18 ellipse_path -stroke -gsave 10 dict begin -165 525 moveto -(whelp) -[10.08 6.96 6.24 3.84 6.96] -xshow -end grestore -end grestore - -% cic_disambiguation -> whelp -newpath 284 586 moveto -263 574 235 559 214 547 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 215 544 moveto -205 542 lineto -212 550 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 215 544 moveto -205 542 lineto -212 550 lineto -closepath -stroke -end grestore - -% grafite -gsave 10 dict begin -243 674 31 18 ellipse_path -stroke -gsave 10 dict begin -224 669 moveto -(grafite) -[6.96 4.56 6.24 4.56 3.84 3.84 6.24] -xshow -end grestore -end grestore - -% grafite_engine -> grafite -newpath 235 728 moveto -236 720 238 711 239 702 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 242 702 moveto -240 692 lineto -236 702 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 242 702 moveto -240 692 lineto -236 702 lineto -closepath -stroke -end grestore - -% tactics -gsave 10 dict begin -184 602 31 18 ellipse_path -stroke -gsave 10 dict begin -165 597 moveto -(tactics) -[3.84 6.24 6.24 3.84 3.84 6.24 5.52] -xshow -end grestore -end grestore - -% grafite_engine -> tactics -newpath 221 728 moveto -215 718 208 704 203 692 curveto -195 672 191 648 188 630 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 191 629 moveto -186 620 lineto -185 630 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 191 629 moveto -186 620 lineto -185 630 lineto -closepath -stroke -end grestore - -% grafite_parser -> grafite -newpath 362 731 moveto -337 719 302 702 276 690 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 278 687 moveto -267 686 lineto -275 693 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 278 687 moveto -267 686 lineto -275 693 lineto -closepath -stroke -end grestore - -% sheath -gsave 10 dict begin -382 674 31 18 ellipse_path -stroke -gsave 10 dict begin -364 669 moveto -(sheath) -[5.52 6.96 6.24 6.24 3.84 6.96] -xshow -end grestore -end grestore - -% grafite_parser -> sheath -newpath 390 728 moveto -389 720 387 711 386 702 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 389 702 moveto -385 692 lineto -383 702 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 389 702 moveto -385 692 lineto -383 702 lineto -closepath -stroke -end grestore - -% xml -gsave 10 dict begin -108 90 27 18 ellipse_path -stroke -gsave 10 dict begin -96 85 moveto -(xml) -[6.96 10.8 3.84] -xshow -end grestore -end grestore - -% hgdome -> xml -newpath 39 584 moveto -44 557 53 502 53 456 curveto -53 456 53 456 53 234 curveto -53 190 76 144 92 116 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 95 117 moveto -97 107 lineto -89 114 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 95 117 moveto -97 107 lineto -89 114 lineto -closepath -stroke -end grestore - -% paramodulation -> tactics -newpath 114 728 moveto -128 703 153 657 169 628 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 172 629 moveto -174 619 lineto -166 626 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 172 629 moveto -174 619 lineto -166 626 lineto -closepath -stroke -end grestore - -% cic_proof_checking -> getter -newpath 270 288 moveto -271 280 271 271 272 262 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 275 262 moveto -273 252 lineto -269 262 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 275 262 moveto -273 252 lineto -269 262 lineto -closepath -stroke -end grestore - -% cic_proof_checking -> cic -newpath 245 289 moveto -231 279 213 265 198 254 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 200 251 moveto -190 248 lineto -196 257 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 200 251 moveto -190 248 lineto -196 257 lineto -closepath -stroke -end grestore - -% content_pres -> acic_content -newpath 442 584 moveto -437 576 430 566 424 556 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 427 554 moveto -418 548 lineto -421 558 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 427 554 moveto -418 548 lineto -421 558 lineto -closepath -stroke -end grestore - -% utf8_macros -gsave 10 dict begin -521 530 48 18 ellipse_path -stroke -gsave 10 dict begin -485 525 moveto -(utf8_macros) -[6.96 3.84 4.56 6.96 6.96 10.8 6.24 6.24 4.56 6.96 5.52] -xshow -end grestore -end grestore - -% content_pres -> utf8_macros -newpath 470 585 moveto -479 576 489 565 498 555 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 501 557 moveto -505 547 lineto -496 552 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 501 557 moveto -505 547 lineto -496 552 lineto -closepath -stroke -end grestore - -% grafite -> cic -newpath 215 666 moveto -193 658 162 643 144 620 curveto -120 587 125 570 125 530 curveto -125 530 125 530 125 380 curveto -125 336 144 289 158 260 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 161 262 moveto -162 251 lineto -155 259 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 161 262 moveto -162 251 lineto -155 259 lineto -closepath -stroke -end grestore - -% sheath -> cic_disambiguation -newpath 367 658 moveto -358 649 347 637 337 627 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 340 625 moveto -330 620 lineto -335 630 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 340 625 moveto -330 620 lineto -335 630 lineto -closepath -stroke -end grestore - -% sheath -> content_pres -newpath 398 658 moveto -407 649 419 637 430 626 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 432 629 moveto -437 619 lineto -427 624 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 432 629 moveto -437 619 lineto -427 624 lineto -closepath -stroke -end grestore - -% tactics -> cic_unification -newpath 204 588 moveto -218 578 238 564 255 553 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 257 556 moveto -263 547 lineto -253 550 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 257 556 moveto -263 547 lineto -253 550 lineto -closepath -stroke -end grestore - -% tactics -> whelp -newpath 184 584 moveto -183 576 183 567 183 558 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 187 558 moveto -183 548 lineto -180 558 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 187 558 moveto -183 548 lineto -180 558 lineto -closepath -stroke -end grestore - -% library -gsave 10 dict begin -337 456 32 18 ellipse_path -stroke -gsave 10 dict begin -318 451 moveto -(library) -[3.84 3.84 6.96 4.56 6.24 4.56 6.96] -xshow -end grestore -end grestore - -% cic_unification -> library -newpath 298 512 moveto -304 503 312 492 319 482 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 322 483 moveto -325 473 lineto -317 479 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 322 483 moveto -325 473 lineto -317 479 lineto -closepath -stroke -end grestore - -% cic_acic -gsave 10 dict begin -363 380 36 18 ellipse_path -stroke -gsave 10 dict begin -340 375 moveto -(cic_acic) -[6.24 3.84 6.24 6.96 6.24 6.24 3.84 6.24] -xshow -end grestore -end grestore - -% acic_content -> cic_acic -newpath 402 512 moveto -394 486 380 438 371 408 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 374 407 moveto -368 398 lineto -368 409 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 374 407 moveto -368 398 lineto -368 409 lineto -closepath -stroke -end grestore - -% whelp -> metadata -newpath 184 512 moveto -185 486 187 439 189 408 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 192 408 moveto -190 398 lineto -186 408 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 192 408 moveto -190 398 lineto -186 408 lineto -closepath -stroke -end grestore - -% library -> metadata -newpath 313 444 moveto -290 431 253 413 226 398 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 227 395 moveto -217 393 lineto -224 401 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 227 395 moveto -217 393 lineto -224 401 lineto -closepath -stroke -end grestore - -% library -> cic_acic -newpath 343 438 moveto -346 429 350 418 354 408 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 357 409 moveto -357 398 lineto -351 407 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 357 409 moveto -357 398 lineto -351 407 lineto -closepath -stroke -end grestore - -% cic_acic -> cic_proof_checking -newpath 343 365 moveto -330 355 312 341 298 329 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 300 326 moveto -290 323 lineto -296 332 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 300 326 moveto -290 323 lineto -296 332 lineto -closepath -stroke -end grestore - -% cic -> xml -newpath 156 219 moveto -146 209 134 195 127 180 curveto -118 161 113 137 110 118 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 113 118 moveto -109 108 lineto -107 118 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 113 118 moveto -109 108 lineto -107 118 lineto -closepath -stroke -end grestore - -% cic -> urimanager -newpath 174 216 moveto -175 208 176 199 177 190 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 180 190 moveto -179 180 lineto -174 189 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 180 190 moveto -179 180 lineto -174 189 lineto -closepath -stroke -end grestore - -% hmysql -> registry -newpath 391 217 moveto -386 208 380 197 374 188 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 377 186 moveto -369 179 lineto -371 189 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 377 186 moveto -369 179 lineto -371 189 lineto -closepath -stroke -end grestore - -% extlib -gsave 10 dict begin -108 18 29 18 ellipse_path -stroke -gsave 10 dict begin -92 13 moveto -(extlib) -[6.24 6.96 3.84 3.84 3.84 6.96] -xshow -end grestore -end grestore - -% xml -> extlib -newpath 108 72 moveto -108 64 108 55 108 46 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 112 46 moveto -108 36 lineto -105 46 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 112 46 moveto -108 36 lineto -105 46 lineto -closepath -stroke -end grestore - -% registry -> xml -newpath 332 150 moveto -327 148 321 146 315 144 curveto -256 124 185 107 144 97 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 144 94 moveto -134 95 lineto -143 100 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 144 94 moveto -134 95 lineto -143 100 lineto -closepath -stroke -end grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -end -restore -%%EOF diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index c5c0fff05..33365877c 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -270,14 +270,6 @@ allow other developers to quickly understand our code and contribute. \end{center} \end{figure} -\begin{figure}[t] - \begin{center} - \includegraphics[width=0.9\textwidth]{libraries.ps} - \caption{\MATITA{} libraries} - \label{fig:libraries} - \end{center} -\end{figure} - \section{Overview of the Architecture} Fig.~\ref{fig:libraries} shows the architecture of the \emph{libraries} (circle nodes) and \emph{applications} (squared nodes) developed in the HELM project. -- 2.39.2