From 0775f6acafa9aa176d148a8f3acf7e750c1c3171 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 9 Jun 2006 23:52:36 +0000 Subject: [PATCH] - added a real-life index page - removed the label 'matita' on the top-left logo - added a big 'matita' label for the index page - factorized common stuff that goes inside in a new SSI --- helm/www/matita/community.shtml | 4 +- helm/www/matita/development.shtml | 12 ++- helm/www/matita/documentation.shtml | 4 +- helm/www/matita/download.shtml | 4 +- helm/www/matita/images/matita-small.png | Bin 5341 -> 4182 bytes helm/www/matita/images/matita-text-big.png | Bin 0 -> 4733 bytes helm/www/matita/images/matita-w-text-big.png | Bin 0 -> 15477 bytes .../www/matita/images/matita-w-text-small.png | Bin 0 -> 5341 bytes helm/www/matita/matita.shtml | 97 ++++++++---------- helm/www/matita/menubar.shtml | 1 - helm/www/matita/splash.shtml | 66 ++++++++++++ helm/www/matita/style.css | 45 +++++--- helm/www/matita/xhtml-meta.shtml | 1 + 13 files changed, 154 insertions(+), 80 deletions(-) create mode 100644 helm/www/matita/images/matita-text-big.png create mode 100644 helm/www/matita/images/matita-w-text-big.png create mode 100644 helm/www/matita/images/matita-w-text-small.png create mode 100644 helm/www/matita/splash.shtml create mode 100644 helm/www/matita/xhtml-meta.shtml diff --git a/helm/www/matita/community.shtml b/helm/www/matita/community.shtml index 1dfd479fa..16e029f73 100644 --- a/helm/www/matita/community.shtml +++ b/helm/www/matita/community.shtml @@ -1,8 +1,8 @@ - Matita home page - community - + Matita - Community + diff --git a/helm/www/matita/development.shtml b/helm/www/matita/development.shtml index 193be32a0..829e4713d 100644 --- a/helm/www/matita/development.shtml +++ b/helm/www/matita/development.shtml @@ -1,12 +1,13 @@ - Matita home page - developers - + Matita - Development +
+

Matita Development

The origins of Matita go back to 1999 and are intertwined with the @@ -15,8 +16,9 @@ Matita what it looks today. In this page we tried to summarize all of them, we apologize for whom we forgot to mention.

+

Current team members

-
diff --git a/helm/www/matita/documentation.shtml b/helm/www/matita/documentation.shtml index 7718cf4cc..293520143 100644 --- a/helm/www/matita/documentation.shtml +++ b/helm/www/matita/documentation.shtml @@ -1,8 +1,8 @@ - Matita home page - documentation - + Matita - Documentation + diff --git a/helm/www/matita/download.shtml b/helm/www/matita/download.shtml index 94ec8dc6a..b992b2694 100644 --- a/helm/www/matita/download.shtml +++ b/helm/www/matita/download.shtml @@ -1,8 +1,8 @@ - Matita home page - download - + Matita - Download + diff --git a/helm/www/matita/images/matita-small.png b/helm/www/matita/images/matita-small.png index f6a234f2a6aac93a0ee707ad6179e54f4a2fe9a4..15b5ac691a5c3217d73e3823b200bac49e536014 100644 GIT binary patch delta 4111 zcmW+(bzGC*7sdoZK)MY;N+cC<64H+Dh5;%=df=paK|o4CVsuESY=TH`Bc=HYQX?ft zNlMr6<@e|Ne(pW@+~+*!dCr~UAG!aTiQI+kCJ712PjjA=xCi2-OeEYhakz{)^G5)6 zJyc2Fz-#<(rlXF*Xi^7|;o`JVU~Bh1o?2YgEN+8Gt5^R;u1Z3p@UN|35xT641<*n< zkIbVvibj-yU8&wcN_S=ni-)V;C{rB^O|5QGyhfqgTRy+skAeU3MUG7|+jIVlI{Gz5 zzb$b#HuZ!u`{96s|kCVQ>-6rsd@=C+@3x2ojhipd@AMXi#A!jBM ziSsw_B$4thm`nMMk(6(5r!re}>8x-Hn&F&VW0{#A2vB#}T9TJtb-z;J*TAWbboIKg zVPq2Ws!`o=`$fdsMI(vd%xA9do^RCxsMYG?V!j;VjkPt!Aqo2Z<|ex;n<_#Uki@-$ zMyb8Y=7!FY?7N+R#NlLpe0^iDX8S@moIhn*>gZq~qN2LXZ3mk(ybm5+2~`mMb$mq3 zj);wA`T=bH3DSqmcbquC`etHpZ{K7svNfnKygh6T`)1e2nwyvBaZLt4_>ojt$di_y?!8Zd(>&;Rs3xD0i)x?St9_EhVe0BC%&VQ1Us(8YeckDwk4$K2 zXt6=Xd&DsM&b5lpb)B zRa+}Hf`vGKv9auDr5fjPy+;ouFF6IT=SP?+CE+P_CeeonaJ zIX<^EmI%fBWj+B|8H@}K+jEtpqykQBKetHRoE`63G`y#5m=by&z{G`gs^)@$q~n-rSO1x7SP zaBy(6FpUxj5yK7)-5V255<-^sZGGvIUESStX9qL95)w&Z@w+xRYk><{5|upNV%-kG2z;<`3udSnlB6CJ_Y@sV5blu$CJdQhpMcmFy8s~rVUQb`& zdp49wN8n;d0>VxOQZsZ7fx8QMq1%*|m2X&v?so)OCz|N#wbUcm>|I?|3-oSf&p0!E z!q&`eqR|xl$JnD7wYHI58o{yTkdPHX}$tasa9^>^6kTH|Qh}B17cQ-51EzlZ6U$a%_|+Bc|`%yZ0Y>pp@r^#aKku zwToNy)ToxyvNF^9cl=;+qS+)rKK)H21Y_E8ihN!wO-^5LaNxm5=IG>dEdq3($8E4pC9jPYiAC?YcTTO-H-LRxOJrT)*u%9T-ge z&6|hnNrE{!IYD4rv`kDLCQ1kdV$3~-8m<*nS9tRlfb$z$`CatZ*}0&&m@HFEQh>8f zM=8YxCJA;ZhQI%7JhCcGqnl$0(Rvi5q zwdvyO$JQ`v?cScA`BrKt;sS!!xaG9~bm6g!DxvZ?ag&L`x ze)GOQJ}D4nDF%BIMDw-d;lqamz{Et)P>Fu%`i%d9+XMY_jEJ|DPcEE78OIj zUdLUp39JA}lXl+mMqX}j?W&wQ5e z@FYO(28!1zd&SpBK7kU;5TDw$mY33AV8O z#22uxBq3`E&yC6ES-0z!u^z4fGvD~cglMY9WIa;7bK0SLaAZVcc@x&?B}z$28N5Gw zWB6Y39lF*K`4Oe1{i zC;7~w_1`HqI!ikmI=Wzx20x4iP-pmNx=BFv3S_efBADGl{gtJIXinZ8BM{DAcu15=glT)%f^{9Ltx2dPGm9xYtf*{E~3{)>) zLx=9(S=GD-H!UtIQmqvow5uAJn&QBmfo^xX5Nzk`L~|h4cs8e|^%3H&xSfchTiyVR ze&N>i_Iz))9ITkx`|KEb*Z-gHtd9kTEm|u}Iu*3?-QzVh1;Jd95i~yU)9sG4!ot+iD!W^(*)X>a znJTgJwyrZ|R#@9t^P2diBo%dain_YGYYa=bE^d@B<`|n$AMNjLICYz#*_m(O1j8t( zsHosuh8(Kpd?gM@VDpnY5Bx6GV$lKEOX(|Qj#l~MJfY&_0|8}eVPWA=FNOE?3UP_N z8$(0fM;e~&N0&H74%jaQQ_J3$k;yD9EDQ^d34}{Zc}iN)7|l&)%D!qIP1WE5qx?KQ z+O6|HkpL6Q`anf<8ekp5^27MM;GjdvI35@}h6Fb^fy-WMY8I4~L}UON?1h@?JQ*Zg zf#B7u_I*qu5^{4*M9D{OSi!7ZrqonaZfa_328ZtDv}^`R1}I>&$pYdfa6H&leh7zzGcIa?Y1-lxnGUe z(C0VFs|dZsY(UG~`w{|KQ{WqSCNrPuD*B9%_t zWUGxXF&VY3jX#R+n0Iz|ZXF!67fT((`bu`haJ(A-{`IeK_Y@FFIh>gBF}P%>&YqO#BKVO3^7X$g8Fp!} zJHS_?o-#BplHkNxK_vWr&kbdLr?made@FfhgXJSFWQHr!*BF`B&~COyJSLEMRs<^v9rf9BFZ>IviC8vg@c2P^V&j=5g|Kd?>#~yBO@t?GLLcW zW6SLKet&Y`2JkRZKFDL8Uks-9#n z2+%6SpC}vn|K83H^hsIC?pJ!{*b^}mQWELXUP+e9O;hR*C8yFYi8jBsYTHBxzb~VE z(vs@y_f1vBIAK$E_Jhyt_PTBP1F}+jjoqFqv)OQRmPZ^RNuG4qI5IM<#Y0~R4_=9l zEq7qNgB`^)xCtj&vJ#GS_*Zk^PEH?o{Q(XXL`poP*@?CvvEEn3k+`T6k=unpaVMq= zc1jzEM8=`ttcElm33*ln11arW~_-wzEQ^cDOI7iF;uwD`T%Kh&Gx1%-;tUH zOCrUS)(gPwwk*+J_q7E!Bn^TXptH9alTdF+yOAF9k3^9wd4Y0=h>Zx%9i_zj{SM&s z+U6y%HLd+b2qAWUKCMxVIDK;k?b(XJy2g2VTRwNcA{>Mt5{Q*($6AdwJVU2B({t>%5`WkF_k`+!xWFnQ%yRJ?n(MyD3C} zl$&^ozvyjEssV_ruCrew>8`BP5saZ=qsCSnC5fpU{vceo8t)EVK-#O?N{V_Pk3>}gUIrVnfaNlYF!>@ z<46irbhE-;hFj(02EE#J0N3|=#i0kcBVh1+ZmVlXt$T>y_FXg~!g(gQsl3wr?r!cd zeF!OjaqFLH{?ZI12~Bhe%8a~$*gPoZ+$xWo@AFe(?pHm8PzmCuY`(WS()suq4!DMX z;S!aNvfnwM%*(u(_C;lp)(;H+kCo58ih^~r##p@~#i-W*cD7IknE+#yl#F?6Recjdi>#x8?#1l_t1oTm**b9Fz<7%^I_ zzn^_io~$?fCVFedUvjq^jj>gx!r~lT%dId+gSRu~L)807Z3ecey3`@8GRBD}WLu|eh z^NN{n$f|yzPwC6k7u}{i35s72?SwJAs09b)h3}$Mpx67rh{m%Jp|C}!>7=K)KUTk8 z-ewzP{32{pZ@%$+tovqHf1bFLYiFGvX{qEb_JJvK**<18j|On~$41qXF7UfWm{X9Z zSAvWmxp~38BgOtwhXE-o%a~EO^fuJb@^vkwYnOwO|DO4vaH zeGiO$Zo}{xU6d()5Ft#U<@P0~dyf11sFX@rH}0BFB9+e`tY7*-b@r547CK z>JOxUBsfYipxW7YM{)|#Msp3IC%>I~(BYe3>$rO93tMH?YbO?~MBbtkFeuT@w=Lm# zx3HS{hDYnbpF6eOAPmCf-1)6u zDC=5l0t@;pYFuTpILMp(0u0R^%B857lblSgc(MCE;_7-1t*EFFvJTI$sCeUz9|hN(qXli$F)aB-MUllh0Rs2Q4|q^Xg`0(od^S>2 zQo|V%(ZT1({K=wzCbhOC_|fby?#<-@HG^isQvI0X(om|Pfsv7(fkDKy8^yXTNW*{I z*n@UMIlFXHVT=_2T3R_zI zy9c~}p}-_jradCHWQIr!SnGWM2CM;QI4JoW(DDc50)`|#mI*r>|6KEfSpWMEJebn0aWn46EU`^1hBDj2kaJx&PK zRgmMePwOr0luhhL`udN3eWk&ygTzoXGs|;V%%ln$dmV30E7yubt*_fy{d5Ow&U1kX ze@{a{)!Z-b)HTNLmCd%roR+;Bk%Tq6$b|Nks*VS469t z{%95;OXCaCzjjPaiJOvt@d)ZRmh(`^q$cEXG{v1#j&WuXscEYhR6T+1jy%$r#at$p zG9}{IN|s`QxoR9Wik~5F~ORG z^1!Aruru49p#&&KQ?T0pDl_cu>l34XZe_*Rbnm0<@^bJZ6ZhXA|L>F5){Hu!PCPa) zE;=&u-Yv*P>E=hBY$oX#Z_Qa?5q(~O7DS%x%noPDB%GZE7*$(UCQFl{v)fHp0#!CT zeN$_mrU`=wS81kGLMCL-U;QYA+q{K&ZoNGUy#EIbdUrwDcl&qW#pyw5dAUAxm@*|b z6}dW`L435SU{88=^B%YgNHyi^HOyS`6MDa8H)j5HZ zk9R$y`bNcMWDOMN`(lLT3hcH&1Vp{V9hvzc?`~c;DHmF~Y@NMu?7ELKHVqJLy;@sy z>O1O>XYL1)%Azk?J~+izKPih?LJ7*N9xjWq$hVsj(R1_GzdCR*bmo7es!F1*t$p3r zMiVwi1Q_1u9gfKu9K0Aa_c*P@8U)eQ*4AF9*G}@>;#)YjzsUsWRIkRbq#=w<$vEGO z-$iFXtCW?H%{cMh>3tzyD#UlV2@?2N7^N69p-KI8r!8*&VpT=}qI`zRPm$}|`Z>+d z-+{2yHaE{43R5W+6cD&o`twvZi>lEvKrgDn|wt{avJ<0qxTt zKMYDC*YaaO-e9@RlC{5eeznhFxIx>K0rhZlA`?NH#YeeGy{B&YnGIGrpCumEh{*@) zC$`Iye*ST{+s^%`Wn+`yZ?F5{0R}tFKhkg6>J>RRHSlfBG7Ahk1sLu(oDB(}Ij; z4+5tn91f4&ly82hrKzdsrs0D^@dH&JwI(gdrKtWh*U1VFLBY88owje=XL5)?YynUm z23GAi(QFbR1M3?u3M-r75Y={btH6=6y9E~)@@G3x(a?nJ6zf|c%6}cths(nxNY76Q z_?`By%MA|%S1L|w0VI%D$}s-p4MuHe7Z<(4%`meLB|+H?zqz1#L@rQ576cO(7B*VO zlBi}G6>z8@ZHB3snr3i9B-XaY+2Gpt1Pp5#g5iZE^!q)B@4d1G{NUG|lct7rNrsgD zErPLexnA*Ia&mGZM5jU?`2Y2Ui{y*qkNZP{)g?kV_)%9IZHX_*rR1TJe!g3}2PoyW zHgHs(S8l4PWvKzlCKX>r!&U6`45#@vEF03gsWg zqkMc0PpqM^fI~i>x9~mj2bm*LpRIRW=8HsT{N{tRGcONe(g{FB54I{~3HxJ2F z82KpftK^6tVC1LTP=bAZeX$#UDAbV%O3#d4w?X<2i*r6`gZdy`FQu6+EiH+$9of-=sr>1rjl$K>Y z{u^|d^@`af>YHE%Y0!CqqojSIBgO5T*IltyP(i_RM30`H-oLBF&>wYckxNGq zE~E)(tR1H<7#}!0+8i7nE-WpL>F7{EP_I$|y|t}j(r%#3u^ef7$tCdKR+8z}ULV7M zyJ~C4f31;CwSTT{U&Pf=<1N-DsC}{rU)Wxr9Sy&iiu;x(@-{b@FuJB2rZn(ixaQLb zdyLhyk>l+zMp(w%z|F~O#52$`#K*@kudIk6aZmb)iDX(ZcDarHJ({3Q_2Fz_loL*p zb?&orb#-;1Nj-cq8GQ>NLf?84eN?1T|Kwc|Z1{^LQ@q<$P5wM`^xHQs&<>|Qu9aT?^8w`CbpQZ6tjPELn1dGuiVHp`5W^_p zu-nIgNK8wMwyI_?;TTVgJoTB1VRjj(EsiKEF80Rt#-Pdd_X8U5;ySQfAtUbnA3gW7 zE1MZIXEE(p=_q{m#Zsn+o~h{|s4Fv*&1RLLZSQ;d+och`B(Ix3;$Q__qRPt3G~jR! z89;^so_v93&zf~FZf-W-!>J;UI;b5bGwGCI;nP~Vud`adY{~EBxh$!nkGJaG6PgD=I*?u>>=G|Ed?c9m1+Uo*xX!?TvBrwPX8Q3!+UdLjqJ_TXNA+5p9U^X zFPT$@%t-#LdE^o}M^u-jpR#O1iOTK?_0KlInqu`wzhJ`*1YDXu&%NiW0M)D1tEUa&h+2?Oez}y9P*KnkQ5db-H|V_8=x*u z;-(+;u>^00i)*nw*NF+$;I1-{Z>FQ;MRx7TasxlYiojLZ5KY`!buC zmzS26;o@cHtU(8+us^`%B*~O}4wGBd!kf?v(@12FSahK+kx%;Fo9!q#AFOUFerkMw z{ly&>$Jl;AY_FbG{ryz|m5@m;Q9I`)r(Gz}UE9D%dJl^3FW}@%B2u`sMHMl41Pbn( zv)7yuWLS+QY!YyOxVF$$rpI6!u}$ALoOYDV6{SlT9^tPXqTh2NB_mZ<#jK!}3{Ovf iNn3}kFnG?f`|qli>q_qi%@z0%Nd#Bbc~Yff9rizBpGBAe diff --git a/helm/www/matita/images/matita-text-big.png b/helm/www/matita/images/matita-text-big.png new file mode 100644 index 0000000000000000000000000000000000000000..b76d8744655d024a7e7f6e3b56582f5e4b1907c5 GIT binary patch literal 4733 zcmV-@5`yiCP)a{I}$Bht_lDE03CEi zSad^gZEa<4bO1wgWnpw>WFU8GbZ8({Xk{QrNlj4iWF>9@01@FyL_t(|+U=ctxK>r2 z$3N#B6p+K=rlMd1Dx#(!Xo13{Q#ysp7?z=EMP6#0cpMFyMrERG)M*Scb#hE?8Z*2w zK9zZ4Qq(jx2)u+;lz@eJ;m+X*94?3Xz@|~W*2Q{k{6)i8<^l6_w(St$hzg%?0$$M~swj%Gmnl?V@9CVBbh#oR zpP$yO@fYQPENqMNt$LEk#ijMN!dG6h%=~v=l{A6h%c# zQ4~c{RJ0UDQItBNOTld)iG*S4i$sd<1GE5JfOWun^WT?&6&~2!1RM(-Wo#|k-5WV9 zZ*y7tJ@6azc|EcpFcj#89C1-fEuH=!U|UGqYRbSnCT-DbuPC)4TEl?uj-R&#*qz|| z6M!>-zX47{;399Pc1MR+>(dq6Bpwdzf|FP5u5e@G9^u@N-~Bt%_EY zDOBqm+S3Y5PVwb;GcRPb<9xg$gHf?dp?c4=hFe9;jyHgf3DWf`l&fbGJb!CIp6pEc zyMofI9@WPKO}U?&L3`z_Q{aFca@KjcO9kLDtQ(vUv$`bOFTbVBkMJ6e<<1 zlgoQ|GgQ4MC%eW2H^;nY z5b#0{f>okF@Cf2j=L^lIH@5=#XB8|($&K;I^ywnt!W0Cn9r4Ish4=+*&ErS;GSVtF zz9;5v$5h}Y;J+h$cQo)Y?wmQ|jJWOsKI6fAJPBFE9ir`pqU6R0fLn+^_1g-(hAcgl z(h8u>q+J!RX+S&*JEvwdvb&@fMXL|+3&hpg2d-zYvp^6dfd51G5c$BlW(r_&PS0;L zBjm4}e=GIDMA(e!Y&Z{lr=-ciS1WwJ2)NXNtvejQk4E4tz&DI=MB#V9Pl2By z`$FTosP8EgwMrf8nj2~L03P*7umBDMrUBOm{QWRso=1XJ;#y=sSk|=)ZHUWvk?0BB7qJakgE&Xc0bVa!q04hks{vWVI?2O)nGSTV@c98| zRCthwHlLA$`1b|ot6(Wgt_%X6k04loK=zLwYC5^E7xBmDIntVrEEL+X1=*xF5AmE^ z1-y-{FAX(mIPh8QA{O)nPB8*i&JTgZEp2`i_+Q{x=HIJ;4WD>E!M(R2Q=N;DHO4i(Kg3ll;^kRBe_sCIxiO|k6s5=vH}x=VZG9c$Jvax) z5h{G=RP6U@jYK?A;$FWHSzPQE(Z>COhp^jAa8svy{gcH#I!r-1*^DfsFar3arOop* zdiTv{`XtT08_xs(fW&2NNN8Ux+3eFw!W4@3(+2fNL?J22E z))6V%*F^k{lPX#&T16AB{=lC?%F0gQvYc(a(MA5|v8Ht;a7>Kv|HSmZ@3E}7dw?$k ze~EeBpt3yr0hQOdDzV#ChOx-ba~swHpSSqET@gnSm)r!LmGB<#0sjIV3Ctwjx%ECN zjMNmxXZAt12nBWaHY4j>x94o96KA!oMQb3@gC*`k77IT`^5Z1hfLmi;(-WD7{5&u! z;x!w9j|1OLA+KHpp0OOIx#APZG-(pq-xLBwF1NH(6VDAp2s@N2YsSp`xYK zGNX`4?3LJ!Z0KF!iLFjVD{Jq;u@S#F4T-FfChwRLR~&D`TacK9)o4XLA=7pt{gX$c zbq)4Yk6VC=WaB8(SKBqEMrlIU=Y!hqE0JkKU#N+ZRupCtKL%h_R>l1OX%R;d6LI5e zzRKbn7mgSMkvM|3orP1#&a+WRT1u^Q0l`rwo&aw1%-*^Xt$9=qtCFV(RO1TZsRG$+ z`y2PQxNb8r4!cuvleoyiv0wBaU7b`(aVD7D35 zz=s0<_I>08Y2O&>>c&2ZRy%USZIM`jglDRC4!0b+Tu(lyDGvY+(Kb%0F~ZKu`=O^c zk8*WmA4KamU}eDy(O2uFvP`tNW_OMiNk>^qEix(K^A$ut9!5ngB{mX$^R6%a6nL&q zDvQneT=U6q+VsQPz9}`v{=o4eZIQ2>P^+SKD}K($hH-5jRhSVL*Ze3)dv&Cx)KeXN z%2S(r5bWt#XwljY+*z;!w18~)9OcOX;&0S#LjoMp2E*4!{JcJywSTERwL&{6E4n>Y*P?TCDD5}Id zPwnlF%zD(EXgx~tPGbGJRu*qX>mvLN{;ViTX$kn;R|mGUv5TPNy=WCp0JauzWSEC& zZu<3Dq0t2QQ@;@I}(?!NIZ!IudOF+dP}W2*f|0CfVOQ)jj~_B=Q}*K z^#C%Mrq4sPo-rerBJo%qR+h~fjn0zL9k@x`HKm5x6!3X(4{be<3=S5~L$nqau;47L z!^-lm#Wh)1q;FtI)8MomSlI!p0${@6#+Iw>RD8j&Lzx}YfaIno;9nVprU>F3shXl)>$BP;4j zWYc1e#WiCxDpND5&)~S~)~}*fVi>{h@L4kv_*kdU_5k0lg-WobfQ9C_by`{eXmL$1 z;O`vUbp`PCI(;XHY8zg6ycY0z0}dmp$Dk|loeH1N2bR}@Xss?_p;=w0m1Q;Xs>O9K z*O@M%zP$y9Y8zg6ghg`q;Z%bwsq74OJJ3`MqE*D>>EEv73S+Yg{B+=N9oTXnaEIw( z)&e$r+EldabEFltzI=YpwjB&y6JYbtaJ1&EqE&k~r}<7FvAphHLz8?j<<^SPV>yQC5FP{DV4=%HciPh}MO`poGuu0-Ou{5=Y)$1)@FR^B$hr`DDo7 z@;Kd~0r&y%(F%XN-;^zIG(DJvQxOl5IO$_K+dMm_y<0rU=jAbNUP-!xwdnAdG1`>D4k(;JPOr!QH)-~PZ1B&c!u{YK?j?{3MtZha=C z4*5h+#Phn6tvi4ZW^B*DhqRaFdo_;<_};Tc60N)!4&#cJ52LK#Smg5};8VbX<{o{3 z6M;#<)xeY(&+m-{=d=~B-M~G-*eX4*?!X16SJ`3ttnZt9jkmaV4dO&H%#2351IL+s zyvpQV+Pq@@2A-o4PoB=S4x7>c^WN_qeKtn z;LbgsruF>w39qYDenz_)eWl6Kp5)&nj?3`0kaE~F$GX)NGVSK#l=4PoUz07fs?2D( zI-;jH@Ic73pQEzVMZb`1#uY`h4k?&uE%HFLCOT@UCdRbm@3C8hah-Njd9Cz*2hVch z%Kwrl`RLLM?fj7E-k5X!nj0dhX^udTH>2X)65OL1aVHNGu8UL7pRr~{9Q4fBkoD3a zk=_cxk3b z9hTuks*L(4`V%&A>;h*t#&~XSzDQ`c6;s)TN`; zl91=_Le}Df*1WqRP7^0Ou&WCavMg-fa3+=aBL&eHm~7gQO80!7;KLoGFd;%mXCo4= z;-DD!Z7})#5Y;_*Um%(n>$EBzmY)D41FmfW&LPDkPgJzBqZi`cmSzLB3%h`ujfew9 zo{j5LqB-?^h+wZdoAe%THstoHGVPO9dfZ_d{xs2@bzU{L{0ec>DZRr7a&(~eyZe8SY5envEpF*6mHBf)K#MSMqh z5`8aQ3$o^1?Vf8*C-ZS6Ncp>E!u)3yt>TFmreeI8aw9c9fjyr^_GM(*sO~mvAaNG6 z|1o77TphpC54-IRX{ANTx}{4VOK9T;+-+FBHN(7KN&GeCN{k_Whofr3eYS<2m!?CO&}OwB>qO_p!79|@3#fnyOgC^{hI9DyY~a0 zNoem_N47N}`}|zy^;YDx?KHhm4^AOZqj(!XNV0XZTN2tZT}7*yqJ=3q_mIxweHwd@ znvk$Szjjn%UNH0QNjVvK5x*T4N=!6UBCZ;tw@h8g<4m%Bk%$Vmo~Zxk*uIOAb*!{U zD6>c&f-8)(9CRReAmN(Q3UfA<%KJt$TTfQe%9q2F~XmFmtPX^u)RF(b^R9h44a9q@L3Mvj6QIvI|VyU^>aTUsNhbbrPf!~{%f#*$GZqG4K zo6W%D#vkqQL>`ZRQg6! zVcIoI66Ix2(>QH2`Pre_l9?d1ly$m_li&85!tuu=26OU@#8!#dF3m7y}Ik z+hf4O1V-*L3Uz`HrW^XY=U_X~-)A*BPr%6jTNll}U@$fw=!XH8oC*hn%--nB=b3w% z_8)?=|Ge=^69yB8q0gPY=07+)5)gcCDRX;X9J`-;@4@Bs?~7&jKL{6IJnUX(`uKc) z@vDT^m*rbaz6W0Q9CqKBo=rGkDqXWQT6}%q-b3aM*(}CqxgUvfpEYU}X2Td2YaMU6y3UH{5Z?FaHx+MEqewA`_T48 z13MGM|CyTsW?K_Ylr}xse4glxx_0aJ&1jg`ou49-FNqly2F4E2tdVlC>(iCOVbTei zdtmhz`6lzPr;X8K#7_8080^i8y;$bv8J)f2`Zri$W~-00B#&wQpeS#ub&1u8O(|-Q zrHDJlXX&?a-g^C-o#88MnOK?U`>_DM&ROE`#|m1VexkDprN*6nDLMI3S&E^x))G$4 zB@(cAO%f)xH9afQKiAKPdstJy)JN15GQfo68DOwX_T3*A91I5iXh|^Ae_+}OSh(^> zCq*6pyx(#LPZFgk^yHn0zb>juO+{us`B66{7BUs?RB$}^K^Eta(!lJhbi#x88S|AP zC!8Lv`6#^>%gxWKl#^!oS%PrHH=iBtuY&1%+tM$(OYV#&H%ii@{sm^VaWi{J2 zS37Yf3aeGTDMH~Y>aKgqQj1>m(SdnKDBeAfJkq}!K36`vkGQR4Eb@R-OwMY0ekR*Y z6p3n7KQQ`pML$_);``1^#jy)fYkqHh>PvM4`G0-G2~O53UX$(9<49P##__IW?_xF zx3t2d+*O2tM|~<+}bl*|M7f^e?ou{{b7`oG}Je@(8U3zboK_tQS!V^M32u2)QSDYIpjy_TlrP%d+Os#NNG~-gaT$y!` z7kO>H?@2|kM^ctEyRPGK@WpGFy-b?B6dyLG5v^I~Wszd|(qoU*`SdML*u~w< zd4&(<+cECky9e>MHBHWR&OKq#=+K@uB0W&=>>}IQK>ap<(qwRg=dV$?{oN8R>ryrl1G9#v+j*x|`5JwYA zuTugJXsbu&c1x9R@iHZQrlJ$#Y0tDsStp30$SE#{+MT0lsiTKJ35GrLIOF}MM|SKB z<0px}&zuXBtfx|=Lk^r#{BkD9fO72Y{C8EfSA-?gcWVEdXKWT@3nd|})8m0CV(8I^ z>aD@_`1o&=(;Tg)V;^pJ1t)R{xpj)=AA7`rDT^;Xc2{duYGQN0Qj*ZO{Wp^rPQUka zNQzUJnh;)0kXt^Zacb%vVYUk2ipkE3;T=UJ7Cc#0mk+OLC3dT}IB6Vr%FK#u*%2an zHwQ=fXII1#OghFxm8h#5bs zzf#>kx4wc3)xEcN;oV0|d2T`hQG?4Xx$nczvO=WYlC?sd)v)l?e#GQH!~3_^?;lE; zh!>GPNszs7)`c7KXnuTmMLuvuVq)<zi)?#*~fqx`q;$2<-+_lV8zpZCxe+fr_c z@*!pou+DuK7(E*xOL$bF(o%%ywny2-FFCC1DfStk6S?b!OZ{DX`A|;beQizIJ(-sz znlO$Eq|&-O0W^NJW>ElNj;OXo6*gr-M$CtGeDcWC*{LPekxMU$p(m$|?#8)HEhV=+ z+QGMMTb>@9*}9pkA}$~CNS1?!V`4v`y&)@aLZ=s?L2O_t(zr`JS? zfqU1It`dJgTD)HGCZ_V+7x?!(CJ~N` zZaqCY5qZu)N1~}B<5RzRv!26?)hdHzq2q^iy98pJa5MJ=U$2O6jYLni9(v>-iugJ` zd1!z$$u#%HUX{Fbj84GqhM}&01I5$IJ1?D3)8di<|Et;;W*2!|i zi-Mc=nO&)`>x1s|G;{izbnbi@P;fVOjjJfTDjyYkJl0E2TKGoHYu0LccJ9JTlRq^_ zIn#ecewI^;S~#fkx4-g!^{?lBIr{Lp0qF@=BVTyd7lTaJ4_;R_BwgB%3EdOCx47q> zWc&p3tHH@_&Y}C~Vo-v1lQC~}_lc(WGSt>Kz3&>1F^bg;xIa?y=miarK4MjhVwv<# z@QqsFkdroJ7ERW2_^3MmWh!6NE}u73z@hki_1{ucdr3CNrsxH@$Ed$(wkkvI@9v{F zVYs)?}UG~cbM=!+Q`~LvE9FTIEpPoUe>wq@hi!x0MgJ! z+bD)w>-O7Ss+N?@dy$^0YmrW|Y&J3TN!Mj0(i1$2Lxr#G8_bkyz1_8Lbi5Yk#zON~ zTcap>E{`)Cu+o0Wrq&h^LqE##?=KKGNcPM=xTsJbS^RhAv3&WMvTXbY{sE9{SyF>%axj9K5W=0Bf2&EvhXv<&G_jV&Ob|{DieB_ zB#GJUYwLVy8}8;dzj&wEyt*Ih}Y-G4dbZeYG)W(k-UZ&N+?3pS{ zC!fC|zvr4=HJ^AmS!+KHw@Vf)yZ>!&{oMHMpPm-ifyaXS0Z+2<#L%M+K_a@HLfXOU zoQl;3xA>U)r9{;lOWQDw(b;vHLTli+L;-NGM7`Ue<=_X}K`n z&me+Vd@C+IxeN8LcKsM<2pSJmA?4JX9KKy4Z#I{En`05&{`9Vo>&Bx zT<(pJ$Hq=v{n3AZC>FKT#$#V^dblmWg-gP##q{T#AF^mZ#9<}M$&C$Vbp+?C=t10h zWgFW6sy`pM<+QJBd_(Xv%O5Y@y-ksx_Nh?|iJb7sH!OQPO2X&2EM7TC1f6Vf`ZH{R zwve2fBW|CX3Im7Ou=zpg^W5kQ_qZWf#Q5AgrJXr~<8U>({hV^zd7>iqI){2|b?f6I zj)hw+bxpr?T($+i26*8^-EpR<6O2d6)%h}0mixN+ACwHKTf84kn+grB4cXT<{lUwx zN-lnO6qt*VZ^P8-9W}k%KdX|J;*S;?i_y$cM>{Ih;=2bOlH)F{sYpMaRY_J=y}3y; zKf|?Cd1viQo6DSOu5H<$V77D_bBagJc(UndKFK_3tc77GhWE^hCM_(dV4e3&w&sCf z1S7Wt4w=tLL_Y{IvNghk_24#ndX?OdaZmxK>g;B+6zzw#^#GAE@ANez>g> zdD7fP{u5=z?7Z4O!7JYLvP?ddB~8sGvUFAPE_c$3|-ww zV;1eXZ=1}#Z~pA>QbGy-^#1Xc6Hg~L$tN`zurKbYv3~7K2o}bO<_3i~^*;74Jh(`F z6zLfp<7tHmV%GIy2tGfa_C>>-!fD|f-6XiLyvtT*-{`b*>QI2WSHr_nJyU(kFLFae zz^X25s6&0)kJ4aKJ8`XcmsQfkE|Sc|>I(LU^K7LYIi_4*Q-Je{!ocQR{ucZ6Bga#J zbewG)GHa#vw~K9k2_EZK(mdoX*Qc;$N%<(Uyl;(fEAEaasVbHbqH%H~ZQqZWpS*I? zdlt+3nB)Ab?jFdTxno3Hqi71zqW+{ExYXV#7pqUeIa($ZamdA|;kJ>@UA8?m$!V$T z#Jh|FlzGmDeh)Y zHr!|BLT~J$v72GBw*m*BW;ojwXh^oa*5+0@ut9}8|}Kyqs2GRtB!Q3n6 zO-qY-?lFVsMdaXzZ+7g#z97t6KCV39+2py*c|~v~DR1VD#V0}eF*aYzCzX{1dF`kw z@tvJ=|8+`pf2_c4w94hj8OO_x`(gettQ8ZwoGwf&lxjZN`FoL>)Dd(KQofSgVnUp{T@H;5KT>oRsFZ~owgsQ zW90w3OQ0}6H2$8xTgE51>|Hw$9EMwc8l&H`_B|`Bz2&qTe@nm`@u8i?&?y7IPyH@6 zMQehKqi6GsD4ZrXDRb{vS}|t{*+m6}%eLtlUM~Ul@{k|i1NV(C9M@Mo;{5r?p7Db^ z2Rp7?J4gpVXq`WWy?*1czfZNsHA>gJoMfy&aYYC)V*g+N+=!+#>tV}fD z2jgZ7^9jHdNDz*oe^E~Df!$5uw;Uwxw}Zj(Pf<*;`Vsoa7y5{{SIC_*nj+DjhXR8Q z%3;}ITGxg=$CQ(o$&s?KaPrJBDl`VX^o2CbHBnF<4+}r%Ld|0Vb2(DM12Ces&qd4$ z0t2iRmonsuK^H>v^!L%{c6FojM$HdFkM)-08UTF=9#MlngN8hD*woLr7-8JOnA#{X zzwq|%;_+oHMac3ei(JrSF4f<73-TbrQwK;=tP@fHGnL1&&(V`JGPxW&T=m*c#B4o1 z#ks_F^HH3>h42)rF$%_cab2QACm=iPN_8&`7Ly|8b2|F{aaU@`wH?8BP|@~Mr&|3EIJ?YHxx1gc1fy1IIn^`E>r~t{+ z0{BYdXza`g2~+0$a(LKsP)^_>z8NOKOG&`Xx3#x(Nj_3PaVg1YIgE^q$YzIO6(>GF z5qAOlIH0cE6nnI%!pmWHpk#OQ;MuV{8*_7WQgl%{Lf$@ppX?CntOR2?2X>~T%FlgJ z4v?X5yGT5k^c}@F8A`U`^oC^MC(BP)c#!%`g@_<|tV_0&u$x{l~DD zS1_ZcPEXbsry3uyXd|?~MSHxs@K7OO;ime+Cz04>`!RAg(4IDUKKuj6gyhxipG}(E zMRqwE^j%|To{@)N>K~aMtx4G(aD@c?0!b%KaH0anHXQX&oGuarSb$q&XVVLZ!%ek3 zl`mkiql+HtAy7)Ap9|0$H^sn_nka46*(4P9rZ!|l?nSr}ldTQhFiq8jOLOz>H09$M z83zdjYe@PhgxkNJ4axyVI8xS;N}s0`_be4~+IPby+tRugr@Br%w57W2skrjuLg3a? z-_lZ_4bLZRDK5@ux>r^Lym4)qkYkuppcBJs#Y1_>uXKVSqTuzTrFbW3P|jA&)P~W6 zk8<1es*>CA^{d&Jj@^Cn448;3hAER>xEhtN>hoGK@aHk6lg;=FvqEdypxk?47s3R_ zXb&n0Sr+iuo~ijcIrZ`5%$XV2LAg^+in#i5tbikP0a$DLq0*?4wRO4$+4Zxnxg&*u z!0k8;$vHNMQ)hXTc%PHBwydK^DccN7#$P(xvwctGe9W7n)k+RrJkW}>r zD7Vh6d)WqQdhjmjM1YAvb37K&l{2Di>`k%XoOS;7qB|%9l)OXRwf1y%C!o9A=U65t zGs3JzE)Z;=ee1rgG;$7_kDGGK88iCMkrEO8CKR?V3Ahu!L7BDqh)cl~X4m!wN@5j|49M zq`!0RFr_QUuftse+U$;xP*j2t+dxAln6PJ$n{zE>BO- zQoANjqz*|ge?-%^;Ukf~0w)(lOX*}<|BpWyrV@5d)5<^TauC9B_wE;2I`_guz5<~{VD?T!WITx6wLgNKoSXt@ikcQj=0Xz@lz1ZXITHsT zirX5B!SV6&ozvI|$c6!QRU=11_~@d8Wvk)o%~@l-va5@5c?4IJkVRzs(+*7{Sc- z>%%=B+{(uCY#sw6Q@^5mYw~HSA#yOSnU^*>nHRRRO}=ahYB6ccclC1pO>2KANBEny zP}t!&=JJ<;83~21W=69k8f=eA`^=46SylP=w56$uA%;k^>^Nl}wZQkwsB}eq@{jh6 zu*pw-9_9@_$>kxH+8rUj#wl@$G|2)ms z3bX8rSuVxh0gm|3N`e2e56VFn`hNy?4TlM``?J7bfdOYmdxoIP^(~~PT%z|z%4%Vv zLozorv)YKh`oB)*Mq*cll@ijunloUs&lU7&fv ziF(wD`nv=~JiW%%Pme_+Wo@yT-@W<#_@_oBfOF>W>|>*EHzraJU?%`~Qha6y6Udh& z5;KuJ6#D*jw9Sdu*+}v1kt#pB3Oo)sPdZWWAt-D|q!;-q?sZ#=Sa#)V+Lc_})JMN&E4rU>Pq^AKUi+7@em>$C=bb@eu zudLUPOM`NmmIcToUr1>OC;*;_5f}#LBEEeyvNv>Pj+(FVnq;x7kLm}TVs@q;h0tAi ze{)Mq7Lo@@s`hcq%h2N=`H zH$b9`gyfuPP6pNz4rVm#CdJ4H_eOe5P#yv}SBleC$s)ISP!B6iU>l>IfawEd2jshi zA?x}2`Wofss`<`*vSoM%7C&2#Yg^#G0I%Cx9&(juvPILQS;V(aBT|-`6ZLV_JV|3LISkO_d*1M}+Qiui#VumCu`FQoBjM%hSa1O*s} zG$bLrzRtiBUZo!;D0h>^3jstq#f38?Lzoqh0Ck;N8Lhd&fBxG?x|psUxG{3-t;r9Z ziUejZ!It5@^@jz@>3W+Ldw4PO_CT4-5iGl~^v#<$0m`O%;sc8Nw%(1BXZBC{jRpWX zt%bQT995iyoNV&i73i@s`zx(o1n2!j96*=3f| zK6ki5g#x69Kbt*y$npokq9`z6K=CieNKc+4C;&l-5E#PAsobwAUsbkGI^D^-V2{z@ zb%hsN*Q_TCld?!i%&!D9>yG-{i~;)?gzu7ryDlq10Ud|00C|O-0FJMVl#{$t1!m^P zl-Rc#U$}6=95Y(!lLwN($9m;UZwziv)!hCjrwfwa@y+KMx>9E=YcDi)QLl6qjz4pS_nfm|XhA!4-&NDMy8TN`(^__VIoP_rM`@7|R18=br zAZbC>!w&-?0O|XvGIehT%UtB)8q2doIRJ%%T%_nW{7R;7vv_8^I^b_9j(V8sg7M!U ztv-uCub?|Yjy1`*IL-9&J0kHMCvB9Np5UER=dJT1|JQj|-?d zezd0a6xwLMeECuqu3?&Q@e(8)u!cdZawdp*q>;Jad`yK&xtlLQjxHbW9>C$(zJGo~ zcsSMhQhz^x^X-Or*Q~|4KZC>;xt}MA=Mq3{W*06*tNQ(Jv0Zf>epgiKH&+nN!7m5b z03}sVo|z0&12|O7Vvm_k!pPj0Oh&t#zk2c#w^y4qN%;vaZEd|@-$x+m)eTvrj&~^D zom6VsX`i9BeWBBZNb=wL0}MGAK!P88VRth%x26ooq*LqGqVZJD1Fc5Ok@MLw?67I) z1koT!^Cvi{_0NW(4N?p+*={l(bK0f%&CE6s2Oht7Kh3sr)%KYUfLr1H{Hop(c$M4Q zYxZcVmRL>#ZurZb>M2!o^HIXT&#B!>D6qfN*z(u7nzC_C%W&OEO0 zpv`wSb;ToZ0r2MzN>lR#G1puIxRBvR*0o@~k8^J~5I$$@$n^0c2*gaV$ue4;=62Fq510RD0Z#!%Xg{Uv zLt7&Jt`uGDj!9Q?7o=;OKD8s2SOg`am-JQti3UO=t`0vi{SF6A68eYQ(88l* z|GUrsP6$e@&Y0~Z|DJMKJ^H^BL*Z1)i5jQA3@=osPakg$@=|bwGgA z@cS)Lc!vHEnCe{#axD07E2Lmo>g-VBNQP#Z2AKGUE5KyCqY=#i4jDS0gCMv=f+}AC z&=qKGp&Y*!1Zkvay0Fdwh{4hR1^ACCfafph&;bStE9(+_j)-p*$k4+74lZP0PI08V zas0Pm=6Q8$--|enX0^S*49R-M<0=k%d}3&IOqp?BGzWfTLh1KdpEt{t5qh}L59|fMrO?w|YeAu}yRRy;K@ceVIhf(sBq=bZ#n_B^3jnOac);3LM zgJo;`G9!L}`t){oO?PqX#fEhtnt08^;`N<7duo;kUC3?EK-Jvw>}*7LrVcZSPve9^ z>Z|#QraX{>*`wn`bYp)GIAq|2t6P#}b%0Zzs?v1smROqZi@Pm5J5pt)pD5k4IzMq# z7MT&c?qn{ZvG_#?=OQ<|ikjqYmUVEE$jQ!D`%qDC<^D=P~ntx-_*TlHmDR{ThzS)riacQH*( zo7~*oSojlw`d-&mWVC~zUFOtvV#Id{Pp(OviJw_UJi$|8wuQd4gSnt;#jT7~;|G>9 zEpzN!J%et@Tz?y`Uc?|w32whP+pAvmhs-2C_+GfC)g?$i}Q}H;Ba2$oO5S2J=F`4fzQO;Lr!p3*-@AURl)t zju~`=&=Au>8VlXP|8p|>2TvI=ewt@?U;EVyzq4Ffj#^%Ys5(CpFi z_!nOh|GSm?uR;5A{atreaZno+_7k;~AV_!_J^;WBkDgt9in?NI1DBjFj{70mDMTuY4fsZ%%q z8BiyQnd4+1NhoCT3e!HwVxW^9{=AafZ}4w#mg8z;Yq3{{Jd3k9iLVdtW{aUCltwX} z{`#fPXQ*b+P^2s#;`T$M z*rG8A7+k>z0BmDgjx&VMadK1Y9(%vYGN(&mIVrTWs(Wg%*d6W%_@s8U>SO@y20`i~ zLwJo__56jUxv{a=WC2fjkS4b*DVeAZHk)Gp7Oygc`e&5OPE@S5yGjzu&EyLFUyj=- zr2(iK$wv{n!#?r%{kAsUyG}{U$jEe~(s>?&caIK|9z1w}fWzMAB6Z;uo<Q)k?^#ealHnECcPFU0{z0)t7S-mq| z=<~Z%?8jd8!(ZJUefBzS0AW5q|KM6ppbry;`aXhrX?tT%N=z*3{U49bRS!U{%5qzC z3MfCjbLWodu`ODnjT|Z)Pu}U8);4rec z08+<~R;zr$38?4gx?ekFc2%udvT-`(-m8DG2_zEJ zdXdei{&azqQ*XVrKa9WAG z;zArVV0zxXIfZj@NF1q~h*gV!`t);s5~tvqSAdXr{Ql{2!Nw3cxus^QLPtQ@y-$7b z@|?gE5q~0BqTHqP+!mn2M#f(*#R&a+uo;Z*{D15uCzjtU3)WuQcN-@bhX$?k0#nuX%&{@PxXZA(G(_dsZ$ z0_}lrKxs8E>7rNk0@V(8eNx25thrVBF3iMP8yi2DwWFXUVBA=^=H{Qq*O>BxQU8gD zfM*7D6Q5>i^@Ui0T)xxJs~fy^iHDx(MD=ISpn6`Lnv5ypOXuqu(4F5tJ}|j{{UWe* zw&eLo$8_S8llgv{SteW)BjKNB&uGPQz>R*NvVj6?Ho}bi6LGPkZ%6#&b7WWi(N`Ci zepTjsIpov%ci6GWc>o3rKzxcCB7}sT%)OVTfJPKKQWbD9fq`FyL73Z%pm3=#KKj+0 zpQkhyEKjtbndV2gHx)y(y*AZj1zvq)h_JQxAj{_CYcM$R3K=J;o_v-;3y$d{Y)Rh7 zVX`Hgu3)T-Z{9P=(8w<>RbXO@8_V}Z%G8{D)DkRN;j`E?4s8PBF&-`dKxKpSCRv~d09hz6a#P03Y0@44f}<G%-LJ1d zv2;-vs)IxZ1Ku7*~+TN2E0HwI+@kn9H(nJ&+(Y(tE7rMDy=5iZi;53Ki|AceP# zCUgLVSFlJ^kQ(U9JT-REjS|bKV&OG{; z08zdW<;7F_KLWD2pwY>Qrfg(PnYdzRsw2K4&}Rg&`$lNEzHtN- z2aDZwwE%>#dA?jN1?+#pGlbtv{}nq5;RyW< z&4n^&=$OZ3^FW8U)W?>yXaXvU{hIuTblwM@)ijVC|7~b zGE;+#b-)@eaS4=9Yg?fyig@oKe7U5U*!hniKZ16SFAWa3=V=A%S5MF=`8sMey3k{$ z+Pa6FnrheNz1=C+lV?KhopS7XcDweJ#3Rvst145#eVZUta-2ZFJ{dIBX1m7ELDisj z$dXB4T;si5Z8+RI?zQk8jUOnEQhJoQxf#3? zy)c`m=3=z+yJerXHKyEPY_1!f&wskuM^&(D$&_RDZ-!6L@HQzW#btv`%h+DbNmg(= znAf=lZWi%Z)BW$e&B*K; zw0+Zh&+63|7NPm<_ zyT{1p&HWm#C<*-&A@mBE%4_47tc*MUu9`aB6rFa+{69E*=0!6NeBM%Gi-3z45P|=Gw z$Vt$^dfck^{5EKnKsM=0rU4iPx~jXjRDI(k>!6$~+XR4kba=NXlYM2K1CKZyGY>Lh zng9HaIxNT~4jg<6cTu1@d(jxAZs=uT-jIzlXyVrjS}q}9A|p^tEVzF6Z}qn=3@}Vs zcF592wj2CGoo!KkbN}u@BPYnconYqucA(w<-%Ks_+)(G{zd6rhq+O`sdO+s_jf#Lb zB+(}xA(<6ef@DPa_ogYh{wr%&>OEx)iE+RXzXk{cQ{YMnfyBspKx&#m*p*EF-DO_~}NkFhSgv5!#)&baG? zWzM|NHJ$$>UpB;>v*5mvu9(9CY_Zto&7m_JEIw+GekK=yHPAT9WCy|E-LU+OY8}P_QEqH+pPe4~OA=yZK*I`_S9stFxjJ~#z-oSw zTn(I$DVvBAl(#1o7Z+c@%mL)^9$K)n9wMpZpW>;v8~q20aUjlu1{NgyKc(!qqgw`a ziwI~uZ*ZZ$z^bhOJp2Zz|(YjX56TAbvvQwb_HhyOmcIBvb_9NzY!nM z!2$v|0E!P10VGnud?M*%u1?gEDwhs=`^CJ(p8oyYmylXWZe!NHq`o)iSEUKM5BXju zNSV>MDcp-+14Y_ki9_58!*u!vUf?Ik8>{zdXlRC7nh=TcUW*bD$8znuvMs**?DS&X zmo~hnrlx)kl@|iG?=`r6^v*4nm5r?|WW(1UE~6VOa0QFS4s0v*Doz>`IoegOc1l1J7F%iXG{AK)pGr*+N z5^V;ThJEMd4v{2=o|w9uWt=gTNTi?#ri(S~A#NYbM28~1 zN1z2)lOQmb(e70TgU6w{!(Hg}UVMexUV&kQg*hAghi(C24qZ|L|CJPO)=6^tOJsz7 zLlSg927rq!3;-)ZqS4=`-)I7rLS`vV9TXW_Z4pjv7M!0Zi-7*b;3t@yNu7MO_b zbu`roZvH*_T_x`T37M~!xjz8`i00oQBzT|A2nb0KP+fJBX=1YbltN?YWtxD94WVv^ zc;e&b<>ZYZc;e?|hj4Oy5a@<*ePHD3^gt7;tB-dC1NYIYK-E-?f`0AhgdkGaat4)O zxb#KMg_lOVcT|z4@z9h7fyt=!OJgl>t=l(~LLbQLpS7k11b$UlHBH)5u{H-tDEzZnLTZvbWBE#3>6RVwQ|CcTjnLPNjY&l7n1>B2; zuV?3vdVU`%ikAAuauDo3W_zHHC34p!Aae)@W6#W&9F(_?2~1yowHeWREbM!`w&LZZ zS=Bf-z#`nmTt{wVSoPpC{g(PpaUL$V*uSWd@nE;WNYH0ML(2&=r&X9RTh0nP-l zb^#2@)vP9N^7RqxsXpww?U@Pw87egpg%YSJA*rmN=;^SUkeLUU@u90DGEKv$pDqrxL$e4YR~O;);S!?}OSlPE$1CB!?@3VNl8COc z2F(nv#OT|6uWFt=wR-bFRCjL5Io;!;8}c8qF#Snh@?YFlf7{#IFv9BF9Jh#itLpWH z;waduvDqeul^ZAHEPrXf37~q2=0rx&w`|hVEJcG2IrhVPtyLqWdMBLL0)iR)7XM4z zydx7oe*Ym$E(-q&lC$#*|6kfH=jGyg+^O%4=KTHG1jH#J6H4(bQnk+{crwnsfJ+ap zUZ2&HfZvU{BPZdsCf|R?hb0__S5(d|&Slr=^SYTvQy^no6z?;TS4bH3>(X(5Yfu__ zcsB|HE#R@aWzu#4`{mR_6E2c(c9+U8W8nVw9`lFr5=ZhI^MaK*CL)^HaHIuUBcWwz z>ZMIS5C10}5uO))_*asI%{lzlxQ=BN(Y6l^K~GdJ z{fb}eWlymAMT=8y{^@R|3^kjeq?CdWMxSqisvbv1oIXVT$#e)0W9CA4sxx{oh#4Yg z2*GjwDuWHqv$pfP~LVp&Gmz9Q`mT&;b9J=0%?B^F=}TmNNT?Zg|=6r!eCw6 zDs0dv!*{b3!Zim-?1pxzdNe_7vZl#qq&p;jQN_G1)Eo?xnLYk;=_>Sb8Jxdb4IA6& z{zRvH{CLq8>zzrpey<~ZmaBPl@4V;E+^tToYZkf@n}(qQ<sG0Hox58<(Q%aqwLa%-vmCbEch_9vN^O zY@xPd#Ekp6SPP?#239h-Ex1Wp=mZ!x9u9RrEtz`6Oh;E-y4>BZlsbJ+{jaTU!))!W zXP{2XFOT;P0fT4Hap6? zD>&_Eg=vH5ti;yVmaC`d>W?zRxe$C8Kj*l6lOPI3pP-KH?LwlTDgRCF3OP&3%F=oH z@=q-+W;MP}I*Ed5OJ zAZoFlPecSwCuFiesmY<9`UCnor?$Oa-rd9F5?onXDQp{AP+9rLA2$xHxy1_EX`)#R zii@L5a)SjQkR9AeD-dspk~l6Txpn4 zS{X?bGBPnSFfxjo^`zL817h%R7f0y+E3O{BGze3riO|W($@Y6U!xx~e(pog&1hxDMlm#0i)V`HnUtF_K!%-EF`x|~JmjIQi_Q7OvbUowS9 z{KcVT%b=|1%;Vr-c}m570*l=i4hJ6}(aFil_#=3?e5Wb)!-o$MV$Jega>~@bsn68NQ|(bb8UX*~&rL%wb|^_#_}e25>nL6>1h11)j>eG$B*J z)16tBIx(>AZ9AJE-axwfE)f8+6}D)6eVc?r|M_$A4UO3Et|Pd-FeU!}zZCqS^e8rn zZ}_8-(^}tURUmGqm6fc1QEeKAc;ZI^I?v-&) zvH*6PxA}oJli2Smzynw*7GIV8P)HP%8|Apwi$Y>RWV()@+o+}x3WFV7m> zf0oiV8#UC}nC|8hm{;lkj9)(TU`mm=Rc&ZqCmShuvIY`uqEB#TdmH@1msV z=H}kad-KU#%worYE9{yqn54C5E&5Ia2LGGXb_r=}Yy`Hp`YuO&xcFBaN}-HhHZ`TF z{BsD~{u#t3##T^RxTw5bdor%0qk~Bq)rlopoSz?yBBP2=@w?(i?2IuSEN zxio8VYw0i(b5gGN68BL#&#L4k?6oH>UaiXt zf>bV$1*!5qJ3nRx1Ug~Xx|Wt%BN3`)LV|+iWk1fezn?0YKld58(C1AJ~ z7l_9Qtucm309nu|_Lo<$Vluf9Q-QL+@9RvVO7;0JKmC!fyC8mVt}ICDT1(U3o=aU_ zoime){yyBmh*szOccU`Ut%CTEcUb>s%Q=x>ULP_TZ_)N;f_+?FNk!oni7}qi@2MMq zuLgTj;S{^;s);93eLLiX>)joA*t?-qY!3&S+N=_l6gpR%T zue%rWu;1*#U_Ayl-8Zr9l7Ra+x7-!iwt=px>*-mECE@UVSyCjB<4i?E6RB5XXa%eI zdAb;>0FflQJj3JmI(q(Y`M|i-u+mFF^!TKW6F=Tz(sgrpHz?YUu;^44lFJNS2yKAn zm6C=+L_|bPRxw2C*(QaYnkU;4s^;dITp-DfT?uxmt`i>3Rt{rulmdTabpF;aS115{ zEx2lH$&_YFJCWl}O)Csa?vs&`3B$S-^8xwmDR(Kyl8=WYLN%qrcLb2vTkXkSWYP-Y z=)iy-{UfBxMmx}*E~~axHL^8Q%qqW#MXEYEflKsq4s|fm2%6@9+0x-(B2OtvYHey{ zw3=QG5`Y6%C`hL*UZ1uIf^L^=Q@={%Ts-v+@RMlz-ExMvDN)UY;dtLm(EpJ`GvU%z z^#EJ!>b5XM(T9hA=k!Try`te&y>M2L-@?&*Hi+M~;tH*Be-dW%&(eHgSyh#BXY$R~ z&k7zeSYRB7L?DjOY{8J=V}9Ou&;yBwSz|GuZ1-Cii$&)G7hh&81bWNtKUq?KmF_D% z3MYNtG9p`Pf>1hC%@sRBE6lVbg$4!&;4w*r9l41l=3WLT`N ztqCzc9v%+c(^XcTK~$_hk5H_#9txe*>EbUWXlT8qC`1mVcDoaggXI>cU9Gs+l4G|C!7=LRoyMM=fK~yO} z%S|~urEfuY(Wp>>T_dW=10&(T{uF4~>MAOPWo2d6{-MVixmNsFEb~GT24RsmO)mF7a&-Of^_Yr~=k!U|?`H+t9`m#4s2` zzRayB1QphXGSyAe7ETUboNNz|juw@b#dUTn!l>6N!usplB4j)PPGddR?8Pnk-d>9N z#lZl>zg=~8lRq~|XF5LBbu43Rsc}}DlGKQtVMqJF7bm0dr4zoUi@wXt!;f$1M<@?H z9Ifs8;Dok$Hg>xE*#yIMmw37c_6%SMiHV7;Yir_gtl9t}fov<`Yz-g{oYzP=vdqsNZZvE*R{C~~#flVYs~wf{mPqo1Xi6Fp~Y3l`zyU%zq#?LU=z z9lCW&IBN$Mu_&~gyr1-u@oo&NPcK(-R@CnH(~OEA4?&k6LqKU22V9FKdHH5{d!lj+gth?zJR_et84sN#|me{6poip=mZxamH&6SEUO<~{h) z_aLXLg&}Jm-Ep0P#N}MAWce7Fn-2qcGB@2~Q3dexfk(gGn@}qX`Wa)+Her8}<>lpC zP$;LYECV#<3dNBpXR;JZvDKYu$S+?qJcWyY4A>J zX>7bZ(x>rmxc{qY&*&w-XQDrjCQ~6$B!!14+jM((cfeCdX!>RMI4-UA0N`xngX)AW zJiOGqc3Q)kGKnP>6-<{Eu(q`J($doWL-_b;OV2qZ@>B1B4=rcv97uw@a`UcM`2Zyc z&J{c6(L7LgP1?M@ca(i3yKH3uY^zf(VVYW68sIA$&Z8Nh;%NAYr#496%zRQjpZj6t z-t5Ja8k#fdx(cv*hl}G)DJdy^ef@C2k)DMPuJ`%kUSuq%%D0(^Vf)DrkB*=^Itf8! z3H;dJw>6+a#ixK-UlLh{hlc)qNro8l2xDI-(6@W%e-O|pe4EH3o06G1e6TV&JTakJ zgNc>=F0L4NJLBE^kzB9es?56LS!0SfS4V%N*4Ec4Kz&^C5F7 zn9F!Jlb^<5G8aWe9u=?bb`qPy7wkYn+tIi}Z1$x1>OaU7eyT?im2j-rPmADNOrJQwH{Nr9i4QKKG^4)}ZEr zQk`jZGgP)~Yir|*fif?7g7nEpn{pE6a71mqV$WOuuMhzBnalIu_ythLYHGBe~?3;_% zTp)Nvtu - - Matita home page - - +

Matita is a new document-centric interactive theorem prover that + integrates several Mathematical Knowledge + Management tools and techniques.

- +

Matita is traditional. Its logical foundation is the + Calculus of (Co)Inductive Constructions (CIC), and it can re-use + mathematical concepts produced by other proof assistants like + Coq and encoded in an + XML dialect. The interaction + paradigm of Matita is well known, having been inspired by + Proof General, and its + proof language is procedural in the same spirit of LCF.

+ +

Matita is innovative:

+
    + +
  • its user interface sports high quality bidimensional rendering of + proofs and formulae exploiting + MathML markup, equipped with + direct manipulation of the underlying CIC terms;
  • + +
  • its library is distributed: every authored concepts can be + published and become part of the Matita library which can be browsed as + an hypertext (locally or on the World Wide Web) and searched by means of + content-based queries;
  • + +
  • the tactical language, part of the proof language, has + step-by-step semantics, enabling inspection and replaying of deeply + structured proof scripts
  • -
    - +
-
-
1. Developers
-
-
2. Documentation
-
-
3. Community
-
-
4. Download
-
-
-
- + +
diff --git a/helm/www/matita/menubar.shtml b/helm/www/matita/menubar.shtml index 8e0043a49..62e98c212 100644 --- a/helm/www/matita/menubar.shtml +++ b/helm/www/matita/menubar.shtml @@ -1,5 +1,4 @@