From d65d42cbf86401347b4d7fd2e85cf733bcd1cee7 Mon Sep 17 00:00:00 2001 From: BookWood Date: Wed, 12 Feb 2025 18:56:22 +0100 Subject: [PATCH 1/2] add user documentation for Isabelle Translation extension --- .../IsabelleTranslation/IsabelleInterface.png | Bin 0 -> 40241 bytes docs/user/IsabelleTranslation/index.md | 55 ++++++++++++++++++ 2 files changed, 55 insertions(+) create mode 100644 docs/user/IsabelleTranslation/IsabelleInterface.png create mode 100644 docs/user/IsabelleTranslation/index.md diff --git a/docs/user/IsabelleTranslation/IsabelleInterface.png b/docs/user/IsabelleTranslation/IsabelleInterface.png new file mode 100644 index 0000000000000000000000000000000000000000..7c0131e13e8e18329e3d662cb955d36189c63516 GIT binary patch literal 40241 zcmbTdcUY6%o9~OFA|jw7^73LpL`0g!(j_j9jA-!(TBJo5Ju z9v&V+qdPY(d3g5ka6gE{hq!NMYA%KTRsCDnNuLDxx#>12O!|3L9>t~>qDS>bo8zh|r7Cnj7`1E$%>CQ#p5Bx&6 zE+uDw>aIEX{b;{V+GWuCU-{Pny9s@s@Ewxyyk6Qh8_C>vm(j{=VvdU_*8hG z-{7$QfyA~^30=icw?4^w8Q%NI#*c@s1dI^I7U1Ub)yxnI90^lm2FJ%!LCpG*tfzCG zA7>w))|W(?0a4M9^`+)tpdlt za+e)u2elp@yBkdnT8Xld@|TR5Fv&aCVgER{B9?sf_g_a|Q1@LcOjB`vou*xR>vve{ zlIw*?>J!y1l`)M?%2pU**GHd4w&0Wk&NS~#yJ{RcerJm{le+Qjhm$8THVegC_FUiH z=-1wmw=H=h+4_w6r2At2)!1>IGFCyK(PbV&*G^%8@L4JoPJfMp^p33QnySbAZu<&7 zaORQf4P2mDBsKeF%md)EYvF1{{d=}{nOqn^O-M?w1QfveI)PYB=oPzho?2eXj0_^PP8R#KBl8`(LYSQRU2mQ;YzI~k=!D-$N|A=#b7OI`}$zcRy|gfH7;M?JQM!t z((W$$>B8E|Mt7!Rzlep7bWTo=`Td5)&+mGQyIOt=LM{iK#j>xGQ{zMFl6R^@V3-qTOPeDO2xACHf^-P^K$M zcA$?bVECBMUTfk?zet0l!T{@oJ3IYZNeIROox8qIWx~^U-Er;ftD+{o@?GS(^47iP zJztg;+<}D8N(?41hR^mfN!lE$bp9|XLmN^zwEG~pC(WvCWcTlowf3jtj4t>XmYUMX z9G68@IXgNkC*Uy}JB>l)zH&HCe&Z;&xN92muXoebJk!xnz^o1`4iP8}+<=s4Df{3{ zUWPV*Yblf6r~ z?UF0QUdef0?y~lg-p$#r7VQhiV;`rqDoX~Ue#R3{#C4CI zUojmd1bYlcI=M+x4IS%%*BB7CMh1I|(Otkf{avtrfFu#Sgj~lr1scM4XXUDd7@)6s+)~gat(@ac=rS9T=8TQL>zmasvVck^ zXu);Jf0*kr=|>ixZhn1tQD5x!SEtim=9i5>2yF`r3RXd>pq(6jhKvIyT#Kd6!}Ima z1$p@d1g9Q>11|FMVn9(KJH4v%E>3Bf;W$1kG5i;sFDscrug4MDC`gxUgf?k$yBvAB zTuv8DO#@#=F;^hs0{TT*0ZLMM@lpPi;!VjkScwK9y{JA0rv;y(+a+etaiGqH(T&iDRx*<`ZyUms9(J zu7wI~l>ja1oDGGuH&8e+?Dnm(dI&1S-G6txLqFNdLO1C?cR%Kt=3U3y?*rq2b13w) zvW@NSX{7~~9#JWHd3fVWf9BJTAik+HtnsRV{crmVzDc(>r-a_heJCyDFY+B8Gz) z+Q7zb*ea--a3_oBSG>ZanD(@fL)0#`_&(?m7kgqL$DEW-yGr1kOV99EP6PYEFA8sk5Vpg-4K1_a= zYss=k+64JFmYHx`^>+=3s*!)M<&IM7wdaVH7=P%;`s%g@t34ZzvOjuzS#Pti~Oe{45HhOP`1sQ4>W+!LtQxn8@C9umSphnq=J}&OzaF4-D7HQp?*c_Gk5;xi zpg`sbe5h_C@r9=<;uH^0cFlnZcqK1JV|MXZ&L>y8TK6>d11wO zqiOb0m1|!xtMJ@J9lcQxgJl$B<0<7>LUY2lUyZ%ODF$pQyBJ%2X6kz>Z-r1Vm@$yj zQ_P+n=y<@H+++k^#>+hl-OQ}$t8Jv|3~O+{>h)b^@i`Sav`GC5 zx2Rvm&H|`Uwm$vT7vLU|y1~&gw##v-AQMdfD$CP|$zfHfjrUc$D&sU)!>_Sv99jlc zgiXuf$m+vX=MU^AfT8i>_lKpr(@duNnj&Xv3zm-g@u`?aUDh5VF8~W(!^{UiDZLkZ zfo?V`(Fnlv!N39M@FzR#7lkD%5rQt+E$?QsE}_&^vN;G$>=V&7ia@d0T+ z{gMf_R(>K$WYqbS*#s~SOx*M|FSL**SL8aS2VL0kt{eQN*vhDGJYZO#NC8r;14ji8 z-Ru{&bN;QfMVB-8$8ZzLe`cYHe-pbFF*Z!ag%q1o#o=0tR#?`bFc} z+p(O{kfZ7P#Fp-jxdaPftOhLi7T)){k#bzXX1@!*pHh78I(;%AcH>#EI{qrx zWBj)*A5&po7fd#C)Xzk{=Q={2#(s&IG4UhQ~frYQ}{DWDWbpoG8DfH$A zU8+hzWRA~N>(-R~z9Ts}kpCx(-M|7oF@;bj*$N(%6MR6~geQ+3?a*@ATQzt8{=Ofh z)XzV%C?>PG09c3WEXAahQ`U(fQr-AOQGd}JJUI-d$ZZdE$jYKC1-nan)^P{W7&uB_ z%!ZP4Q-HZ5jDW^N%&#wa%~`<}kH6gA6n$9ax7K@zv8jN z45qPdu;}fSAorrge~i(SfrH@|DiLskH0PqoWIs?l+WA&NQQCx>D_4L>w?!df+gQPiKfUwLCD^Jb~1rV@5 zO*r638YDn3NB2SU#dEM~dBEwQD90(ZrA4ExEwp0jw@FImBT&PT`c9~G0JXX?3yjTr zi$Q<%>%}8OTS%K*frp1CMr*thcD|UTyjolr1e~Fbu7)C-Nt?}tl!{-jsy55C1rsWY zZBAo{5NoIOZy>;outB8d3MwOOv)@2C$>Bnyf(d8$%9LE|L=4+u>3G_A_*STRlUjXC zY$%B17m~-^JAh4N-cDv!g?R!;TJN-3FuXT$r@?=m~&f=^=H z4D0`<0K?4cN0yAZdl34g)`uG8Tf;8F3>LB{vvk8UN1OozmKT+kp?<-+l%gO?O}$`? zQp<;m2LPHU-=Ra9)A`gnZ)yf%9tkCodlrgDDg7xz>y532dW8ebT;A#q$_2nKnv9Bq zD?WDn628cQvyhACW1-p%&jPGIiy2n}c}*~6sR^&q0AMSVA+})@4 zDcs}rkp;1#mR21cVS=cFxbYP~@pIzr^q#ESF&c~Clb6|>bL!^*NH=oS|3GgZTi+8q zZ>0YRLUj)zgirSDRrZF*@qhli|F^*XSB25UwXJv1Ky77iX*?HPP>n?&lm8LI-sfxP z^f~L63&(kmd|Hd$fpFPVdoYM3F%tr+pNo3Eo3zmDKff>g*iyff+dS8tR*p)e`~loj z{zF6mAN1*8ZEKiSyzBr%qz|E7JhIMhR5kw@fXJQ-GZJFWi*7iQ-}M0?;AAG26@aGR zqK{3|n_V1ep&8A?I*NJVw*LE^{u2L0*v3Wwz8S4`L#h%gaTa-U=`YAO+ho40aJ|w; zKKF-?Nk3ax>y{F`bAt4FtWSie^Dk)g!Mswdxf(0n++?*y3Oy0&2I4(}K?_=CPO+Hx}^Dj=X@@mH`ZUBfn=lFUz+_=q74Tq(KoS1Jn@TZKZY#iXZdx2Ym z@q1iE>`D?SY`hXIsWS}`b>XVlRIS7^|D6i{Um|(2Js;8YR^yZH3HKV;B|-?^_w+rD zk|%Uj&(k65cKdrwx;}IXFDJ9N`P(N*t|lcSZ(XA1*fJiHJa>-`&G9C*+a;76um${k zbWE-q%`51-^yv=kz{m&56Ix1Gt7^HF-h^QrzssQy+_1a$=1EYSq%JQ;WXcdDxR}{7PzO?l%z6)3mBRRe4vGOk zX2wS9K*?f4rxQLcbRc2rcN5AZW?ZA@3SE?)uCJX;W6oQ-^|mKjirBu(#Hn^G5BYOt zOq|ZzXEBXoRTJ|h^@SEivMQl&)oQ{Yd3K@M5Fd*L!PA4x;Hqo}9Pk|CV&#|Rwkj5e zvb)ZZrECwuTXw9qn7WXJcc&s(GO)4Nihzvh{VahYXgSVLM`R>uE~L0t-`+FJgmb99 zEDXxHoQPAd|KV0l3sZr1W&T8!Pa&>B%8dfiAGI9r5yv|AV+|b;^&;Nu#PjPp3+~1B zg13~V*vxdydHoEcyUSUU%k`&lrRrhEiaV@>S#@-0%Zh`s>yB!LOKP#T4_ww-PT$3| zXh`1Qx7hcur0lK@xKVnh{RekE4s_bM^BMFOA#EGZY0{N}%2H z>m@srK45*5KAqmuLC&yIc?wi%n>Qq9!&K{5Db)c2W88f3sTuNH!sgHho`zjZ#N(Q^ zNL8D{aAhWF_X8mv1w0-Ro|HAK_LOOLeAAss|2yRpXDnFf7kZ> zcJ)qEsqOI+N&a=cbe1TrHDUbhme2>xIo>e1a<%mt;HD3K*g?QNVPj!o1Ue(8KQ2QY zCHWd0EED#e_-z|CC%yB-BIaO>MJCmaUMA)~ktJTWj8r2D_fX7zcVSEC`gQO^E1{q| z-MqZ7o~^9ga7JoVv(Ny3H`a=TpGW6`H()3}a3UfWb)h$r4tiD;^j@y392EwF^{-aD zDx)&LZHbDi)`w8SXXV#>BKmQNgK*_|Ryc==7IVKp#47V>*(ENuP1`?2gHdO3Gt3kg zlu|)A3xUUuYtkm`A$?SzQ7UMrX_(kMqpxFj%0XNSpD@@o=UAoa=<<>Q}QDS*i zG;7tQW;rW>JYh!e=I(H+QOQCywZpBmXQA%>=kJYpZ;4g++Ma%1_p`3+rPl5jl$UH> z)KFpwahz6)t%u5ycRr7bgGA4yJsfJn?pUMkSw|i5ZU{^NPP$9+!ueP8%eR`;x&B=^ zFIFTu!j{skLD$XyfjAVo<2Q_vbunCmWt_<;l3qnLH5Ut9SMI`N({}BJ^%&u7j?g|+ z@f&)VU7F|5rK!vYC5%Q(d*Mq!1j-dzuKG~1*<{z1o8{gxw zlDoduEl-}j9cm7X$#l&k|5+OXsbvhRUW(K4Ua3){JlP+eu2*%pFQhue1*TL9X{_Ch zgB0M-en~v}h^h ziGKfjRUt(fQJ`uhe)r9-e8&lYtPkWIU`iSyVz%BXg@uK6>&l&o;}S3 z0y1!(TJZYc>!bAzlkk*?d5qjIshOE+YNgVYO2@MZh}4QmwKJQ$FpT#seqvYTf}+3o z@a*9FAZhXlM{2YKrTH7SpWZUf|FuW+;0?NY{dofI?P=|80q}i`z-3({_o%iy@LxNT zHuaphr^i_@o3knFhC|WqLW3#O>X5|lZT{$S)RZ4_Uq>-E8Cm&sdTO`^m>FSGiNSviNK1j<|eEwTNeo`2|c+0%ND} zVh}EHKJcCY%ohVbb3j|K6={04Ejkj#Xt@e`m_Pd+R-ad4#b6csqde@S*X>TeJXz5KRH(U-*@bjX5b(UR`LllT z(#H2s;7I3#&u)Qq+#-t|bS+>b04E3WWUgKEa<<(Q~}%ed~b}B1*`M1T9OWftNaT zGig|YbpcSje`L4WX>E9I)LrSf%=&?s&Q*Uj`MpP8)tnaVDfAESq}x@uG2G3ABd2@w zUk}BItvBi3S}wbgRo~p@sF6@Cc5vI}RIM5FDxpZ*wBsPAb<7*vTLM<%1n)DIY8848cfYK(0o-#dK>tp-c!E#bP#5y&*F_`u~} zQ2eY)LK(05QN98L;+VPaTDyt4ktKWGKO1v3#a$=#LhH?o-`ct+>hZXV5}trNk@YVH z5%iKc1> zo@p6|zF-|Kr3h^*r&jT>s?;paI_igO$QQ|fg02WA{&=55W5VwV)szZ+B_3Ria2$4W_tIIU zkTyHD^Ex-xd}CQ zq%XwZ;rv}~>QRcAvh*{DRZd;Kp1MQp8OBmBbR|KE2GS`hc+M%^{($tK6?kTH!a&0V z2M&PW@ndamU}h!8m!#0QiNnF(i&QINS#s9o>B*Iqe9TUKODq~R{8N7dg{$8R#Wsbu z=+i&MB={OxOJkip?Q!9B#SS9rC5}Xtetz**C*S8eP34`aChO~*@6Vz}2T3==HnVv7 zU_l(Lg#Ov+-A^6$`nuuh6i}RJCJFS>VCyh2wC#+KQ*=Uf3i6)m>30N=;Z4jru<)x# zVFh2G@pQY3*K)+ha$*)qGk{YoPrpqax7C5r1P>P6C{+KuN03;vx|yDEqsCbRL%n(L z!H^!N+)2}IAm@M?>5&}!=Q8W`kluI>MIkN0FfCg9cKGfnEN3h8l228O%+u@Gi4+p1 znXXvB*8wu|Qyz6LV-&nZd(p*>7oNR!kcxcqbj4t?uLZ^z(Hg*Z4AxWkOPYSge>7=F zqBiTec7y4csM*co*@@P>hi(MwR9rP+hwQtM;+}Xb>4gebE}faxeXU{dOgJ}uIW51_ zS(|5G8XMEnr~zaZs569WG)vNoY{Ly$r-##D#ida#4*@MF&oeSZ^n;9t7h zpeet)I>PzAGKaH8UnxZ zPk8ulBUgoTW$dx*YyT)=o?q8Y{;LS_|AD$)(zV*D2NLXkYVBr7}hbgdNSIX>b6 z?(=0>h#*bE&wfEik{jX($vn31*`Kx2yzk5;!%0&+b~kJv&vcvn!i&O0n@&36z~zth z*k}Y-u4gtZ>s(HXj|>MAxVY*6D7gKPlG3cGn3`R9X5`D|p&X<`^ z?cBFvxu$cr{%S|ahwzU2O1E;}Yghlv2>MC15Q9T2Kxk|yva zNf|?RCrpZVe4*WDKEwPs>|>`5{i3O;7WEc{W~qxP=3f;E?Nv}ExwD1zt8fXbemquZ zR;M+13cb_a-p6dB?$#l$NQ%A*x+CULa%$|M9wga;q?B_i9ujrXRWzOU`CWNUT`kGu zshE}AVaWkT{<4}CpSiAANdx~grnDr zon|H&uaokG!xto$L~lh>%L#u?V#~Wvd48Jm_goaeP;3z$P&H&zSrk`nh~aRv#Dfa_o@zDZxOSI$gKhEm~)YJFoF;wy`A}HakmpkVFZ{ zZg%*e-HqI{E@|*^UFobTYI3`Rp3AAL%I6pY%gT<(9=FH5*9y;aZIf|=qzti8S6Ik} z{1yuQu;D$L5SR^{o0!>jHS5;5w0Ie`{^a+;C2ND?xNfyf@v*HB=Vn*+{ogrhq5_@S zf&a{(=-&LLUs8$_K%T^!`B_SjXg0)Pc$dYRRW>649>WWeO6_^cI73XpJ7?D)85Xx< zwGcR{(79xr3A8NX0UojbgdJ6O1^JX3=vU!RMGY!n^R+O^{L2lpw-~SdvlxqR=xwLn z>>P$d&E8)Mu+n)(JS}Cg5x#S``BleCDg_QNoea!Bvi+{ybn>Qr3HuhFsyu=W#h>Ta z@pQG6G}O+wM3C3J0B#B4iW@D~{vjOWkS$tp!OQfA22bKSu4Tv$B*!(8Jkb8b4>cEm zC??zVA-!1Nnr;x!7)L#1wk|~n&?m~_cl+o|;2RxD`Yw8#HuS!R==R~}fc&v?<3}-i zoF9K!R&qz}ihP$O>`A_Rji2ke8ovGKsqRL*cH^Es?dC?ANu3{M`Z9RV4{&U+u(=oF zp3GEje6?QRa%~l)WEv``{QQT@{{LV5`Ilu(yZkCoQ}~SfUNJncfBs{pFWzw4W34=< zh%U!<1L`w@GqtpOzhFr%l|x(uO*;6v=@njJBH>n4XjoGsh5JRGTc2CE+)P0Ruw&eb z{EwSPcfU7RNlW~%Z;q+FFXNp%GqwnPkb>jk`E!8d7YN;e=2&0RFkhZrVoeE4xEMm; zB99XEF26c|muGJWDt*5Jw|~~Q`5XC$>rjeZYmB3^40w62nQTEL;`CWb-ktg9|CdTH zN7|M;l1w9S{&U3Ty#cHWh;Q=mU3L0;@~{9c@(AM}0((C`_sB-%;eS1xa6d7#A^7h( zZX$#Y{(sMzJ24*cPtKn)IVVPce06AxSIc8f>MMb8cJvU++_$MD7D7KV=HJu2e1`@C zvSG~+@p>Df^L6?UlBvYcBd4C2t~hZ-*J#=ki(q9ZA@@2Ytmy=HP>GEG-rGL{APIU^V1)MO~BClK&WtcK}g}TA5nb0p}kkGD$LHeh#2XWuA>!9 zxcx&#uD?JJdw`mp>T-`{bx6iBW70!N>uC92=U1mE&VobwkS*b4N1CAQ)qSjQKBU#0 z)_GCyu0Pu|K zd||P3ch6+B+eDpjh}l@T>RiXU5#mK(GqZu3aI`{wUS6ICdD)JdVPTGhdj)J28Ud>b zX{np_2V;6q+x>WmTwOOq8es$=oOmJ{LM4g7kzbQz;6=`{B zsBU#7OF>gzkDdmf-^W7xB!IL=^S^J43WrjZ5?89&YfZi3{OQ%kFx+@W;OEP1tu)74Mf{E*fkA?AJeiMUeZmq_?{TwJ9*?Dp+Ych}-j{ro4o zf>(bxUv~`S?eK^xzL*p7)@Xt8K?Ea#8da<6=-Ho|=K;T_l;u93^gBZM9KRED?nQ*{ zO=P|CTYL=GQe#M8(L#IBr7Act1U$>Ov_$M|HA@IC^=;{ z+)%Q5&|I+(oI-Y%FOm68J~k~iftz>wV*ph$dW8!BMN4q5{^he062^*)bQ7lt z{)MG&VCadC;a@YS6W>2}Ms1}&L{i*cyI+;JZ8c65QY$d}Vcsdgg$SNJ^K3Uchf!mv zqH2qSziIxF>tjTBOUwhPPl{L^Ef5s|!RKElwfCUtLQr zys?J1?a^=S80QN*Eew(e^rzMKRmu2gtzR0fEVsX~q0!}HGSE&tnyjLqAU~roLSOjI zRCsK0V%n~chG}|0zN@c)zdNLs0c%W#JKv5_--1P`>ik_$B?Sm1NL-!P14xW}>q!;R zrKFO6f5Wsj4h`jxh&cnQQuMfE;of3YW}~QEl~e4JPPvpj5YnELg;zHTOF7a`W1x>P zoQ(4q&yAoRLTRQp?=}l&t)e`wja>rlc2nzoEk3T7QZFX4nMg&W;jk=*;GjVQKtu^PXp~&`@Vp5CCth1M6&?i+S=twI0mGD?Z`~<*eT)O z2f25KEq!k=;vL57!FK&VNnuNRzkO)^NSi!0ia&a?@kBy2tjRAiX1ky4KNe`t@KNU>Uq==_>l*L|(x2YmVYQNhPanBNKsXyEb1 z3E&w6zFkqKt2d0-iRo4m*MhLP=5+&O1GgkfyY!M@79MH$acc8ouC{=0n2foy2F6C_ ziVg6z-NJ4{3!G<56*s(5*T>$!x$jNamapH{axnh%)sUydwN0hVU9rTb6L)150rT4i z?Q`M_%D!A5*oe!KYHMV*nU*O_qov)|)~V_w09~Qhu}okDJs{Y?KI3)o#ro=W^zHLP zz9xy79-!LY*IctPG9?QwG?K!(R3seG!)@FLm zt5v)B)iX{x!&eV+*sqQ2-%oXeO9|MH#O+C$j1uCDCMjWw7Ozj4;+!dy!8M6g(@WtL z9T3PWqo5pYC9h7JU-|U=raWs`w2xUUx;nU?uD-e;VfV)BV|lsI(bR;<^}h>UW=kO- zhO8GwW4d0v(CgZ2-p5~P0Ds)nuu~5Lj;kr0Eqt6TsH^KYW^}n@sgeEKc5IXaSsS74 zmI_{~iMqn3#8iOvd8BB~P}kxs=T@fE3saZXJD%N(2~uVGmi8q*FG?1SXXtcJBr`Td z2IZ8tj7*%ow%mEn%A0kWr&|KF=f-6Q4wN5TzId&ZSWl7105_LHGG^pN&0*omrQ=yJ zLui_o`^e`W-jM9aKR8n*iGo2AZY!BL+QZrjS-`DnenTLJYJrS%L4I2&r;N#kl@Mdq zJbxf~-AE^xOSkObfG@l&K{*t~5Wl(&K7a+$c5lL9W8sCMdoq4~Qex#OUtmtF!P;}I zM^J4K-PYbVZ=`-a^Yr_!pO<@g(8l8Ht`qfXw!81DibTpwjv6&Ky81MiVP)^p%ghfu zWFE(>hao?7Z_X0)}3%nSg+C6YZyzlnWyyJJ(8P-g8((mLKAr^j`u4pIQLxOa^EDT~^vtBIna(?UPRFex%svHa%JF|kp z?N74AW3HQ`?8i1tCBKbQ4i`U;1*>0Hess|gPfpR${B44J{l`*D%E#%q9FUPI3*!Ux zB%Jf=iqW^XQ*Hs?3hB@rgWiE+Hi6T55-eH$PY-mSoK9PVmh`?ERQ|g3rU;im3rl#T6;ooAy1!ULIxFT z6sPb~pbPkb9KzGZQb4*!_29`rCah4`gBQaStM2XpazHn1pl z|GP79zjgk2%}=_SmO^fLNJxomj~04fnE1u5!>-6mQLJCkr(??Vb|czUDa;v)IZA%+ zbc|gU=M4OM>ZRIz%armpzTL*}!;?`}9o!3>Z?8|gDdzlERs(yGwCHzy1`^~4F9In| zV!Zd_XTC^Nig^!rtIc_K7vCz6{~~tqk{B9bYq<5p00TCCSP3Un@c`(=m%>76){`WM zfgHY|TD*gtG~?|HF-#D6=H~WD>s#Q5ZSkNx!8RIDw4Csz=_tkH!Jm2Wdq*ZMZyN`B zxF|@aUiN4?vdv1_F>Fk;QB2`lF0&UZa~qz}fy~bgU(r7+DpaK2zILJQx739{leHet zjCBjC1mK!DAtY^s@hZdLJ+SIj+^}k6K-Glu=O9o}eEh}NU2V|{w*>XwfgvX1>+)i0 zw#zMDXFYSTKtoCi(Om-VBFKxL=LB~=U&Xwho_vKvJN`T)C|Ei$UZlOcwFIv}m>k|F zL40$ap`z#PaS9Nx_HpYb-`6i0cdG)LCbP<9HAgSfokcg7R^tUtM!LIS65G0oMrt*1 z?F#*ax%=4;wt{e)rLK3(u-tv1cAebQ_%kMM_qah+=j1fBW0%A^A(4a@=KcFKBv_x_GlAB`?8VG0#6N;Bow$BId<9`FalMM0_OuiVRIsEt7 z1wlp#A&0}0>i8`l5O%fuoFW=?=C8%Xu*c>0t|KR3O&M9$KLW44vZ26CiQ(Nv3H_;@ zIqA$P^6-J(8qK(LJxigDw3|P0iwUUhq=P=GJ!zqVNJ0M;San5UmH61<3;fZlNL~ZR zA*buJsyc3~pKTtxYlE9}Cem~W8xJiWSf)^{%Mxw;x>I^XXopHq(m#KFbFSsWbda%n z&SZhumw@VjH0z+Oi_6LYfuPVE6x8^>mk3)Oq-=$rR z{BRH@NNZ`wClx#ZH?#qA5HoY-k$5>NMi7Vp&U8$R_y@_vcGZBgx~<=SXpJW`weI;r z{wMv_FXVsx@ce`-cKm3Qmc}_J=4%mX1Hf({;>q3DrX7>%-k#R5xie;F@Z2kqCnh$5 z9fR**L*LWhiJ$DSyy%(gm`Uh;pg0kIP1!T+xbO~Pn@0KWO<>lis_bsq$bl|4y97Ws zZttvZDT17&G-#;^V@l7&4gHVO=A z;7!RBurlB}vd*dAsirVbN41Q|$m)`BdUA=0qtI4G7&_42yrt)cgO9Mw-&fb((#2DU zFV&kiFdm>x-A3(rE~vW?S2fn1mE7d33pRn)r`P$ZL%%Afyd595botx@k$T4(Pvb^b zH7;7EZUP{*-cnPS_d*Op!qjsMAXahCEg>2(}sI`x1?iu{B5s@O;q2p;Od5 znR8zbeNA-K(i}}j0mI23ZC=*mhpUxR%)|&X7EZZ;i%`F0$OJunnnIpV%l^*NnHr-j z?c7wlRT^L`TXyX9)GX10>DM6JrGM$3N0sw!j%lX$WDzmqE4>^cw&{XE39V#5hRC%x zBC=2Rf~AY`L&mqzVe*O=A(0r~Rd0vuGH{T`X}$36hOA#SoyI4Kt>v*kiR-{N$k^$> z4D|SQkCF}%FQ~s>y_s<(lOh2Mik^zKiM>A<_xLbCw{N$|cc6%9H!*P>eD~lyiE+~) zay_f;{p-5GFO!-r(Etq0#F)5gf+uA>P>sm22r(U7RmLNcdp=oJ3Mk?*O6JAQb4BDWQq>W%8TnkDh|Q58+%+Ol}M& zFOlOImpB79G{%p+?C0g=s?@BQ&|1HZmw8!Nq1fTso-mqn+%T9krH=mL-Y~4@( zQJYR=m~IOVX&~2j__ulTQj$zg$jU*b+zL9n;ua^J6iZDGZ}a#kJT=jKe!y}4=~<(i zd9YH(QZ=?%q3V;ic!p4K&5Yp@#hqOFbww@>6S4ZN&hZ-y?o7L0*~SF^d@FoLe-9OS zk371bxO~#C+1isJ=cWko+c)>ZA8>|m4^mWpEOO?{{WR1aba>~Q&_E>j>eu&U>n38- zQdjrwu@LlO_S7{mnK|C$2?|`Q^<1PQP-rKxc@Jd&kN!sWUy^2z?*K@PcF-P7xf84X z552z7$gj9l?b#np;EDS;?oCMJ{=Mbu+A~G^zoGsM!2gyqbMMVP2;_FC>o$HZbeNat z*!gW}PE!U}BKLFU)0sD+gCT){8+viP+yc&sJ&@K{(0R!CW8TIMVe+4G>7=ti?c>Ro zWj0;!M6r$4=d2R;0s{XdO!WV~ttb9}i9?bdcdNDhOkxUMSFmR>LY}%TiaYL;HDz3m zDO75QGEoRfcI;rB#4T&r$OdXp#F8rdMeKgnGPuzeW^l0}8&W`oH zZ^ml(sN`v5R;oY;S27C|qPYaefPSFgMO*qg1TmvZu4sjQ{nIDGlGct`F||K07GPTl zF_lP;k;=#J-=A2urZVUOz9-}Jw?yte3;Fq`@=pb-LOYdg4bhttUp@upY{tCrd=oOI zraB-m;WW(Dillgbb)|6yaV_#s4}L{FOdjpiU8r-EgSPq;zlFQ*7(1x<_ei!_ zNM@@`9S;ti^lepEcDhDkox}YHD~WjYzhfoi|1~Q~_R>vp=P^yX)@5GxJh{%=6LqBQ z1@NhEZlS1f%5^h#k>d>;8+!ozq8uT)t zOmri5HCk$LD`Lc}y~Gyn9)0n=CC<6Unsc-`H#9kYD6_r?fcF&t~xh6U5LgDKm+p8IY4Xj>DA&-+YGK&5b0S*}#dulpZh#O$N7hl-XB`H=KO zLJbxjuj|tL`IcB6hVIWQlq;3gX@#_dc2Uc@!aJ4b4iL*nHYTyli{2^ojmCw6ptXX9 zJ?J!HzJRnmMwwJ-3C%0I6*{z5*s69Zw+t;0H=U@g zgRZ?6+Lqty7-Af%+v>V69mdIeKJY5MIPnX{pfR2G3w~DgExzu};MPs@i#l<$}Ye3y{){E`>> zatF#*3CEM_?`0Cam8&#d=~U-g+pU{7G%uMSGj+tYs7+EAy+d z%wC^Y7Z{8GW{-N}tb^Bn*aW^&>kKcu$X|pt)Ns)6-(w`v|1c6=Qumqc*DO1he-;b|{B>DQfTV8O^uvkxcVXdA z`O^u!ys-F{5Z)7(QM;qTPd6Yffi-w7kD;GZGtX%;?GMGVXRVoV-~jd zdgNBz55&~*5enaQP8QwoankE%?cyJ9y3JJ`eNH~} zFEEn$pTLOY_P@Z0Z)l7ng&DJ|8qi&G>$fyfFYVrh;OmW-hZFb9%1aE`8D`4M&4pS4KK(y zqiDm!8zMBC`$lf)tq%=a2e8g5yCs=kcsO6sj}scRpv*^Z3Dm@(YjGQ}Px=x1eJHV>M5F8PnKqX8Bhj*Om2dI+%}ho0+)l zul4cjxU}Y>+j9;LbEn3xDDOJ`LPDwQ-b}g6atA{v;jpCX)G6uE8PUVOTr5&waK`ly zZ@aCMz^PY(C`DZGou0O?Yq!jT7OOVodt{%lsnERU&IWZtGa78zz4~vqAZx(7rAGSv zO?fO(`jMZ-P|HN^E{m?6v~KPLZK76P%N?qP92=Cg-O@=gbb>!FZvuC3ZQJl}yiE2F z+@t@4jWv%CE7Q`rw?cSK<&8{&cfU1;l7}zeM*hC>$F7Al=+0KMb%B8&4uDwnvaslli}8$ zyl87t^P~kZXvuVnI6*emd>ra+nRl72O~^Z$VBR#WeOdP9Q`0P!mZtcT7VzAcaOCJL zNt5jJTi}sfj@4~z8{&fxrxP0;7pxc`Jji(CW?%P(E& z^c<2NOWHfL^DE*3;KII=cO+hsA0<%g*Ch$Ehi$Dh#+uKVlSlw_AS!B6>w%hOEYA zil~^LKc;j`5D}e1zQSG`FhYL+a&#x@ovHj5!Hsk|X<(968!C5R`J_c)UgpOubExCM z^_N^QvEY3@;>wj8W1r&HhKXY4)G2!|k`~7VV2(#@x`r>}6oBUz_Uwtzjjp~G|0b6r zk-zGG9bZliD?1Vu1nqh)Yn!d`7owx@XFByO+tlaMG|GK=TAQ|J6ouWCVtz^dz9@fS zVNw>VrO4re2psDL%K!9N)&JlqKmUWH?4d#g=@O!$cS6$0QI8t*yteQ;l}mk`4;B;^ zr7#$$yvU1jl2Z@xx_n)++&{t%^WVAFY*4jn>{DUd)l@jrdE4t}fA6CHo-+p&NM0Uo zy?6fNuvVSiuWkUhz5mWnDy`~^_V|eu7f+YeQ^wU!9sZf{eYMkPKYT!_LW%e!)tt|X zI!f<4#T07%WaoTymEbkiX^gN7mIFgZ@4{w|V=W&DCTLm3mQ`P0t#aZF8fh3GKW6lw zvC53Qw#j_55$&ZFX*sf*G^s{ZkWa?kBG6;%yZ8uNh9e3Y3pz^+jQ@wXH;;$1Z{NqY zs%(`c2`M5%5tCghvWJj$5<^+DjIj+;k+Sdm*mp+O3^SvYeaXI??95>7jIsQ#sr$a4 z`?;U{c|Obc_xk+hWoEAHdcWV-cAm$19LEXW!|W&S*O=IK4qGTq8(K8`g0Px1?Ov~I z%6HGXb+`7bkXXSyA{yfQW6P-iW`eqVP|c>ONNeBjpP`!3FBMuN9}Zs)Ur+PtKhziK zm~Il<-iE69CXhb(F~W<(cut(s2u^m-o`qj z#WcEd+w)DF&l7CyU56V{j()k{=0`8}DJPv+cbs8a2_*)Bv4RC&Xzvd!b+TaS#0II{ zddYT-S9S~oz?y2jn(sBFv&s}hu4Eu!Rct{{`p0XXnT1jB&l=>Vw;Ayxie)$$@+Iyc z7u09Y^7G2H`E(N?)a|I3ScuWkSn9uqpGVVv1M?%qjrkEfCRC^_9Og=>)wXJgH%mEP zHKY9xF1|5pQ{DU#;qm6z(#o18>O*pGqI6pDL+@R`a|{d#jE-6jp?XISRT}YG>8XgK z?VX}AlZBY7sN4^ocX6yBnHd#4z6z!{bR4#RA?gWSbZG_UVjSMp6ZfgE&_L62*u6WT zLfN42IHA`gv%C#cYOA^WDwh~E#$Zyfr2DIy)pLobNu>SnU zXZJzlQvlF{XR+v8Qz^RFg{$Fv95-74nkLP$SEXrKv-0Be^Mwmuq+AtungNz zrb%lj?)Pr;w7cTDyHnZ8Lw=O-DvX7854rKK+HBj1w$yb_y#CE`S>uKH!1_K>U z06S~X2z`ryK4b4}yVrz-2PJxT(TXd{x<|Mdad>Z$^`>FSOE8Y!_4gaQTS#`0_Otyc zoClHwJ{a#Kek*MVyQ-Mjur5GSfEbsS!4^Z4gU`>>m)i|{`F3Bg_{L^7CQF-{S!9fI zm&m|0W1V%-m?K59Kdez-Gqcl83WsY_a(UWE0WxZN&Be>sHhYP2a2oam89_K~Eby=l zRpMn`L8Zvt5qRi0XKDFf3JjiRU=VY9`OrC&dH}UK`@D&Ip>MYZq76T@WW%bDiugF+ zs=~j2@^$oX7ZZuXK(q=73L>4>KoQB#EmJ)V}}rOVVU0=P|%p@IN(bJ{NyjG{muK7bmr@xe0jxH3ROc^7L= zVWK47$#QDU{zZHIixJM>A~=8Vpu@Q2+G0zh=onia8Vmsth3Ww)mHQX;M-^`9O|Y2l zlym~bo;>Wx!+yWWl@AnuGE)8xnDjd@X2kL^RjBeZQ2_?>1}Q%MC0ujc3pFfjH@rwUB$4TOfxYLrDXPu z{RCmWSh$P+f5me71?YI5Z>FBnO>kSZ8;s^FVE2$)lC+wMYMCv%?R3V`=7Z<7IBat@ z)4CTF`DSM%NYcM8;zrJQ&q96gG2tP9c)QX!NC-}#uCGHqn7(C{QpOKYZk#*qrN8YM z0*>Bl3fLbttX_A7ZB`-8-L6opYNx+0fzJ5^#$^{dUKerVO}-)TrTT0ysjIJtORXiQ z#nIZz$||DWYXd`?>H#W&mWcQa5kgXclDFZHfmR2|jlOw7Tu zjq&vgFM7J)la{P`^8)3)3b1N#`;WhPKFW)}dR6$D$yQ+CdUL(*hL`%d`^A@E++LS$ z9;fhgv=ykCBHA}tc|1WCPb?!y^ldc3XXZx-_~`I&(r`70pPp*l^)ZraY2~k@=6E<% zLax2buhnkI{mr@oe4Q1Kh|W%$7u1*Rt}(LNjCx-@DOq7$A?5IP7-ehHT))Xv6jgK8 zOP5>>l>H5NW^Kbg5{c{VgSR^*%4sSxsEfoN3!xkK^o>3>y>V1Kwq{I<9xRB|S!-SB zBu^bOSks&c1|r+-X$Z}8G{T(attTjU6E$9*XJR1Xo?+QQKX?Ywvle_l7um&eAuNb4 z^ZYtFv+(m9C#WZzbigG3xdXkjf>@D;hw8`njgni?FEJbK)Oi^uaQ_t|GFu+MK?den z9u&)_p3+?-J_RlZn#R$!7bL}Ri0b-!|h(+p$j z0)c~t_hFoRH2I|sazVJ1FHeOK9+kEGJheb-_WX+=#0VWgFJZ)u07y`7<1Zx0Aiheg z$Rw{)U!d1&*u8xVo`7g#T0sPmovPBj(Z3O8)LBnCbWxr2(aXnWThBK@Za*=@fq3iE zU-6MU@6MuM9a-xBm|8fq_R9TWMU#bnL8U-N4Q>Vh+{@`PFYhH4oA-Pu&G&^~_3eHg z<;=DBiqc5y=uJVU_oHQetd)`KPlBL!(I(Q`y;r31+dbnfK(Tv-NjA%NSUba$;Gvx5 z{lVjkW^c*eAx2isgxrYDQDfv6ZPZzZyn!0`vRhXaer`3`8g?9CDXLv({JlL& zJ@-A63!6z0=^p^l7wwoUI={#NF4C?mnjqQoh_boiZ$hMhQpum>3aD>M+z zIi^H-N&gOuZpWUF_^p=$MvgH~(CH!x(WJ?w+q?}GU%jtwYCJeF@(URg=$DDjFnd{J zuIOf$u#@$_rq1j?mkk5BGlj($qXT}@X3TrjtN)2M^QGrwgE?6Yl-Q57rcbQ-gdZ9` zzctlBG(MRV9!>AG%c)hAy-F+I4e-T|cSSEOs2Jy&Rcdu;jdw>5jZBv9Ts%fFnm=yg z9a@$n=LUOku$n<3%yhL%bTivbK9;kW-ePC6({^s8GX>aTn05T_J~?Jm=G{U#8bic! z%rI^?u@g49@mpW2?nSJ=4;YO}H4xMz&qf=J{@?Iq2#GOWc@&}y>fATGGazSUZ~1(i zb>% z)?7uqBqHl^gCMb3G2^5O=YY0PDAvAT&l9@XyCUJFEs|`;Pr{@Jd^sOi&dVi-{EZj0 zkXBAS`f!opS0ll1S;gSOU$wIj6%S-?hx!|V8-~(74u2laM1HxW_q^2!og9$9x~)Om z4iJdwLZeg`^65-D$GjhK>NMCtEtxOIpxnLEFc=%mV`R=5&}_(u{tmIE&hb>&T5u`K zV8(<02ER7J&{mzk-u!v&%&t);E$QRpuqyxlgK)L|!UEcW-2Xt9(V^M49)K3s3?Gsc zsL))^qkS(uX;LpX?*63_G_TO_u&F7XXEqdS_5~&(D#@?pC3>iKO64EanEWQ@XMf_x zkW>^b@=os-=@RY;R}!B*L-($P#tY@ED#Gm(dNAsO`DXc>iKk|>9_*JG`5lz8Erznn z`*%L(VPwd&T}Q?U>|{*Djs{39lTB|VzSx^#yEgvfip082V{tduJ;oLw2gX_PQ&juOLRZbIQCo zZjrvsu&r*vqy)hut7fFGenh1AZoT%ZhOulI5>C!`Y{1Ic_C*`)1Xo`FmeCCwtM*nt zIvFcv<__mB^uRVMkt9AgwAgp`e_{UKsE{3)lZUChD9-Ef?Wwt0-5bZW-Dc+=Seh?f zCn`R17JoEbC+5bq!q+!?*nt*H}r`G zR-I|%tcZ}eB^B!Z^W@to+En6XKsNLT@fZz*vmDUKgfNK{rzYnR<;_73`8yz=Izw}nk{-=*KFojoooJinDtzcE{>?v;ay%>_;~s)ao!{9+sR8aL zG@q9;#L=r{=4Y;-8!)GDQZKd#^TZm(fR(T=S};kcIH zZu5hzAUFGxJ_ys}>Ka|**QvJ?0qv0@fb-*WCnV7w`k#TNPpts3l%48-dGskh#2qv{ z9CtzPvnuak6%eziKo8elm+(z;?9jQ3RQGQzFDdx}`gn?#d_fn>Hh^FpmKiK+C?vuf zinb6BkNP#2Nwf^%9Qvk3P~``S)gz4WX6s%AN@$!P)hL7=7UcPdpNTlbci{;=KD7PlmNIjn16uQ z6>mo+$rB3snfh+V;lF;a@_lJ{zTfGdqS#?&{WR6t+EC1A-S3}h8RDv+KPa$i$ZzW3 z*e0nmgzReV_#;5pbTKHSY{$$3M{SHvJK=mq)P%{o3t<2)tcJdLg_Fyyt7?$ony=W` znJMrGg9mG8`W1P3{k=}mB*+x!7&eEM6Q_S!!!%)p8mjdU&iCh@YN zL0u^E$3C6m)%wJZr%P;b8tE?|Ji2+2QuWEZ<%C|9QT0NY8!W2#>gv}cPWz$@`?X7B zk;*Z&#?~Q4B1FcLzWu@WDv9r(`^dpi{b)DM0Px@n+{E@Og~($$k$u)hH0RD$)&G+<1R+Wc0b=`5oU9;&P&qV2zz~7loZuf^I1TrlTD*eG4|xUKQVch zwIc7Q#E5jf^Y^sh-GQ2l688*SFYJ>5`eg_5cOFk+NtN}z04>keC8K=BGhH3kHNo|L zuuvPxu@m?8>Ge;g4BS&t*1V?zEsL|BX6&0qUv%PmNiC@MCw!<^D@i_o_lthtQ-mhp z^|;czVsCe)CfD0quF)>$5(wHjCpjGAvct198GBeGU83tZd3fmVNR(ndj7s4w}AEQl?pwB;RVUz`V4G0n;zye z3s|XVq*7Tsq1@ix&^GI}?HmTufK95s#q?5=>QqPn4&fmiX1$T`^AO=5V3AhPKft18 z)jxwp#A=7f;jHpedBup3ZgB&KApMwy_NtwFL(>*F*a%(Xg*ilklfU5x=@+9%czn1- zQPtqehf`xAM`EwdAVYhttuoU_&{5IZHTQ6bVC4lVXJmzbS`Qg@cmiTZ5+K49_Sm$U z4Z6%WQE5XT$ccEv?&tX0KJsGS$oh3prX4>$V~oSZ#tAVBI@Ag3F(_9v*dSYZNKVjf zsth~A(^9`UYUs_#8)i{RJ+uwQ{h+-rC~3xv>T??*_$vx=_s$;MQQ}FT`R99u2}z23 z_Vrl@Y%hLFB@buXkr^$&5!Lf0Piu@8$MBps?jVldv>ChR=H6w0!SC6_e*+ZR53EP7 z4Qw~4BsFk5wMD_W%#{3!d=M5e@NPN_rpn~7crR=X>D zSQ0vL4-Z@Y(ur$KjqwtoHrb9^fbYjHNVq;$P-uY6)vByU44iSBh^t#o9~El;(atP< zkq5AT`X@$F=(Ge7O!ROb{DHlV5FT5@is92+W7hlqb^qstqbdPe0FVk5|7Ay(G6&dO zbtFp+5DuS+ZdB8G7lSv`v(v;Y)cEZO9p8H2G&+nVT`Ai7(;9})qAV| z-(VUs_*vjUC#@3DteNGhN<%wsDpcyvKOnuI1artPA(o6S$9nsk(4V(LywwC<#;TuS z&U-JKR(X9~yF#UkN}sf2^>Q0LY(V7ER{(TUxvyU!SxxfsnVIQ|?k)?VY%5CA#OGl< ze0#6X4CZ{XdU0&e>xK2raU(XcqQ=B0fED;UJS>RN&8}VGgtk#lT26{MQGO;@4`;ed zCd{9PiCpa(9?IH0PPH0VbL{{V;(_c44I#L%kK#+2pKKg3dm1f$@E$8P#MXLf6cQ${ zpW1~{_h-s@e{QfZ?PG2iK&))t{Uo>8VB2(l1fEc?VIq4p0lqtPXCuG;Blt?fXm)U0 zOl*f6$Kjh{|2u@FK)Wwt%AogeF%rUt6Vo~Xl05#8Ajv7_i1xO2-5v|EhaS(aT8Tir zMtV8hEqaniG@7Yzo=o0fYJk+AWpbx37>at;=Gb(WZ5`HPn`I}xvgBj4KXtb1GS?g- z_=}1!K?}h#u&Y!q19dzdpSmGt(Reo7vmPuflCn7&5pzS6hpjSK<4`PnJ>-*pKJ8KK zg$DY@@3p$~tnI>a`HZhHg-3*)Yr!97v-&{AFn2FY7TBd<*vPV;QAb@eWUY%=CP zs;PL8s4zc9uCs2XARQL{KYCr@8-z7mD?qG7O=Tor4BoAF!QfwsMhVAeCP9-c_v z-A3~t(&_3l4fghpU4V*dbLZ>&**y>hLb(OEYX|9veVmVr4ciWhv8~56@U%;*d|14mr~U5~E#>Rlz*AHd*f}itvC{ zmG4!1+RF%BU8%(w+L05XC6CD5r81(6D80UK%&egrV^(jW&}T0L;K8ZUYZaMW(_>$K zQCZiTqI?#Nc16*4?aRf*FGQr8#;-X=0ZhUQdy&Fz=G=GjRn5(z=kg^h>IplBXQ4#= zo0MNh`h^g7ua0JNW;F+60 zGE7D)lej6mg}s_lE*mg>+v4nz4Sz7UbNvB16su{&W zmU}LoZ@d}G@mT3YXeYevS5>$4%JQ3 z^Vqt)UfhkisCJ?A;H&U0Y0kp+>gnYB9}nJirA2yj->1q#=%Z3iH1Epj3$*_yCdRz* zc{bmF&5)f!cU|>PYbE&{{VK_&f-F1U5?PaA6=V~6d{4@G9T6*0mUTZM_|$gUk0ZQF zAA}gIoxRq$_Y+>sJ1kFbkor!GGauyka_TWexV?gR7XSf8Ljt_cx@Zl0x_DmGeI^l(^;N_iTwgL{NK>LH?JrO zopNP++Qti#IKgAbo~hV3A6``C^1|LedIlvi3a+FmRkTLlSbf1v%Ws)If2l~<1?z`A zRHNdy{b*z#k}?_ik$B9*4US299U;sxH!UXbIeJ3JkQza>j9ha_7&rZ*hAe-Vc z8e`u7=GKBxG;-7$@#JVvAO3*H;o|`F87kGVf1iO0c3SK%5f`1aglxt*7r}5}fE{e~MLFHp1Qub|2%k)zPNA*9EKT{Wp28RsphJ+N8gzSnFtikTV7Ul~=TUtlj|isTUqH^^Ws{w&ghs1X*!KZ>D@G0R zZls=^}HZ-aBsT8YHitf>V$5 zmiQ{{*8GikL=wo?`5mrA{HCAhS@#RgbQn!5T9I(oZN8CC$U=KI$}G>YlKtMX>3?N7 z==Y(rf&BF(^jfr1{jUs`(YK}&%(BeJkd?ksi4w)`-~!bSB)h~$}^?|U#1l5r642W43}R4 zwRkzP=S@P!q_Qc59_je($ANVhC%dMf#>^LgON1T)CKWz_!>^o}Rum!ScBDZSV4Bl- z7X|PMCvh~mQ$+s=syt^~3ixv&4oUH*qjkLst% zLRhvSuocz(pV$Ql9|w?0AS$kY>>~R=*ag$c{}XnB3DO;qz5LmAgd9Lm zn7VRf%KxpRD#us=pr^fa2rzX6f9l-xKTb7&3ATUgD!vbg8g%2Dib?)|Oy}fI=A(C% z2FqK}so^4vLqa(0qEfCX(K5ecQ;CEzQ1pa1Y_${-Wv}VYqV7>;nt49iK>?VQ$0LO{ zmA5x#q@MR#XMHwh0TEMOfphjKe6yt&$L!|1CahmGP?I4bV=P!@7bjIi_*n4TYtfcG zJ?~LUO+)*mKw-giQQ8R zZ7(AZWsk74L=?qPGsMLRi}A@;i@da%`4sMeWgx6sRgZ4TMDKXqS&x;Tp7YNahcl4pw;^?C-{@p(@+5~GISOZ>8N`(;jpIHpMPFkoh3-Hm2^y)Q&Wk9l&; z9BVLfE16w$Opp-Yj&u8_Xg^zuh>_8L>) zLAfIJ#)A@7IL8WcVhs@m*?~hHze8uu+}nlu80(q zgzOzCLW`D*87tSA-goqO=sa1ZJ3cZ`h}rT|Nvz;wszK^CYz2$Aw={dYHE>sc3z^T> z;PMji?j!hZRMCMRrtip1%p~#zA?%~8-1o!$_X{r$4 zB_JN>^#%?l`dFD*mZLbLIT;&`vs=CkisauYl8w}CMDOiD9OuKkAx*SlD)t~D3Fv`+ z_qg@=!uup{KuqJS?WDT;^tHJ^Uc;7Ev(zRHlCZ12{Rv-{=J zq`tbg`ynY(ah34t6KhWDFb$tgVhnR4v(1>-jqu9jSP)flZblMssryNd^1A&wLJhy)?K3I#G5Oc6&X1UZ;g*qg|e~r>FIT7^z_HH#o(Dl zCuVjXR(1xnL?oonF>G7w>a}>uH8dBzfULq8B2WdVd z;B?QR66)XWYK%1w+1JsBV~RZVQsLSu(cq+WbHT-o_%WbJUK$t*aq{&=9E695+@j{J89^mApWpE8wPBSf} ze~lqQV!cOTJnobU-J{R$Yx9m$*(J>73w0=&eWfb3{)T?R2o>~lQI_kAM~j@fA&3h( zK4YHA^Oh;JIS{*#`|{YSN(#Ii8~qCTXV=t^^I7G|$0UJG1rG&=1J{=Nca-g>Z!?ht-vBP@?g@E z(yQUSZeazOP1#wo|L|68hIr3B^ z-&A$s93O9j9&}J;)^^kTa>U8RH_t!BG(myBQq=pCoNUkFd$g?quSNr0N;f!qwtG(= zFugWj;Xhtq>sDgkH19aS(PDmiGXFGHIDf?ILYL=RMW~BjPt)fcvu^_|a&6}op<*w4 z+zt&Y<5t8nHQm006ly4?Z%xwMI5mSUuO;$mT<4LM)r3eW@om<vfj??S%Y8%u?6En0~f+rz_rY_?L(hK`&L) z2m_G7n%vQhobhZ`9(&+od9elvA)K0&bsm30H__z%G?&oHIzbx0+I2^CslC_Nda9zs z%LFAhA6zXP`T7|B_Ri6%q}ey%TgyQgrfS0D+11xO+O~Hz_AS%QUOpRWTaE}IBtev| zw>7D>?=sltHYC90NrK>$LD*!kt#(jc)w#z{P28I(u@RfEqf*d;Y;n10pF{~-_-3(c z5w-^yZ~d{){0#5)z_ROx1ZcIq9iM%8QeU$#xlrRghJ(Wl`@{P-)s#)NU5?)4Pz~J= zPLGqQ<{DOoDe56eqj!rqv4w9Wi#Y0n*zL#YraurE5?CMPE)!XeEwSrk zQBB^wd!p+fkc?G}R-kkJCVR2YLrHETRl+YfB6OwEqN+1KRjb8<85>?tgVzmSjk1`C zn1q*t?S>(}vkm@rQpQVowKp&{4hJGHdNQ|PI2gM?&h`)a$nf+OSF_q_GE_X{o8CB+H3VbxP&WH)D58=QPc7YVhP&F${ycnK|8(yh8O#j#81T_p1B6JzLu{6CD;QvDUbp{s+6k z%`YWb_WjKcLpB>I;2@!<2wxg+8*|+n@|s;jy%^oUmd_4eOgJ^YqBh@k**d3n6zwzt zBcR9F?@28m87(#-ZWf3{=M=o zGq(vL#9ZX`(|E%9YU>?(>1!IY&t@hcH-coZR(o=Do|%Jqy}fR>a&Lt^omL!NsWAqr zU+(C4bJUHG_ppyde8uQDMA)#{-%j0LP9Jj#kD2`He}fLKf1c`z9rzl-_v*mF`kl2H zi_?wL?p*QES6UZ2;M)1B*5kdi>&sCyanfIB9RTwQq2heF4QA}r1U}X?$xr@Ho%znD zX`E5KBeuLYG?6OHM8CYCsPG;2-m5~Orc;i2>~M(7YDrcoVX16W&7ROs$ZQdRu|iDnj;r10Hmqm8%iAPex$!A|iHr5s2`U@+ zqX{QPm)wn9;qp1$;%^L?N@DJSl1pB1dJV#fW+h9$-Hc{KmiG|1?*Iq^nfc+5YMAW& zSQ(!=2leAQ?9)-RSMZlH`mk4xXUQ40W}6=OsKMpIK=yE*`MV}_Z1R7zB)$4%q5qfB z#6d^xg;k}wFth!U{*OI3LGMp7%mOv(N>Y9F!8AJHhvX|vYF{-+xZoaUXv}Y$&5a{s zDSth{@6-SSt0vf5R=_ij$^F45yo6plS3stH)7`*$2`Afj>$-aONYe%3b8hoEmyorb zgSLTn?A1jYP>~b+q04OWw?{fF_xsw~&6bINc4#}Bb*$g~gMZEPlYh^$K_fpbLMY}m zA@hc-bkfgMC)JjgLwD%Q)%h#F&7T|oK~FQ!Azojy5aGBuE6d-a4nxwquB)ZQKfcW1 zH&AY&nYs zx(yF%fgE2BBMjvFp@7e^&%IRcgRgQbUi0rgf4Uy~bWt*3ird3)1zz5B%}{mP+-B&b zi^_#YlsYHip+HS_nU)jlOmU*50`vr-AAaEIBE{~>oW9jWac#KcpgJ3>@lz7;|Ii%h z+Q>>@wKg*_7@zfD7R^3s3E#tIDI^3ss-{9Lv~+DQsfyxK5z_Cd@oV^LfOiG3#eb{3 zdVvRkGfEs*(JKyzs7^5MR(FoJ;exa}2kxwl-RX8q^!z_Ck+{|p$`SFzJG)F&RH=J) zx@06iK7J^p6#O&M-pOnm%)U0?>Tdb03wNGkJ<#+C=fB}rJ_`8RMdDs>u?@A{E{7_= zZv&=$u7A6D9ST!{ZKVXp$DA_tbp2k?ull-9*ltXI#r)E$*`6)muGm9)g2Fr-OW2t; zl%;uwo>)cRmeZ;JZn=VPaZKMBrI2fNN<4=`ftP9hg91O5f~$Gf&2wf97MoHrSgmQm z+H>;Wz&+rgna`acRnW7A-dgL?5rkOK18s*IVRbf0RLkgh#zD2o?Ft<(XvPbCg2 z^Y?q7%v#L%is%S*r3Y)UC2L-Xwi&OO4OK{ot&%H0@f_0;V9k*J=wpzfKICEWI8e`> zSb5k(RRSbwc+xnlswMGKj&v0w67USU@?-APupii@!l#d{6n$+f|0!y$>}5afp~xO@L+B-lbeCQt zg6V8U5ez-#kdWr(r{HJCR(Nd!O%eT|3L9W{_pJ@P(bZ`(TN9}ZDYcpF%;a_X@F|tB z!)gFY$G#iQoz>6{VK=EO%9*uW^sr36i=)A9IBNR&$Lb#J%{13uA!MZfED{PTc@zQu zxHlIATVCRHSx)o~gs_FCzWOhc;y={nT4zL^qM|sj>%we;`Zp@M@MFCv?|#s3MG`sz zyS*l>zfgy-daS3PoMKdHQ4&F^hj!o9XUmRW0POX>s&LXG54*a6({S_c|4+()&&mM9 zY22=SwqD&*9~#7CKmvy5n|mF z^^{Z^=*v51+Gx3Ujuo602A+no!Ol;>#?rEyV6YfCPp{`)!dk;Of@MPc-0~x-A4q*; zfi*N!bX4v}p%@Rfnec5@C$Ay^d{?`EEeUgLVo&?Zg@!4X>?)}TqaJCOrA@pdN|w;y z6~rVU_jNYd`Wo*B@E^a*%Bn?cpBt=kjGV_OD&EoCq?|7(+q^uLj#azZ`cPVcwdBPf z@K}$%FN@Bkl9lpS!jZhF=r6t8FJ4>j!Yo<7cv4;MQ zW8K}>6xn0xiVS!wWa+(%-__L-nVwr#_w{1pdzxOctCuMs+Z*e9%yV3!rbaP_OA`s4 zrL6pa^6_hRG>QFPldhP=99sCR;1&ZE+#VRb9Tr6PO5SoybxjkQ4$R<`wYh(hX%TwD z<=+(Ceq{sBuXDNaqlq~EQE&+qIOnqbpo`6pHVuEuxr}h1fXTJ!Rr>RroWz@nhvL zc4J=3$h?cLz{7gIKitX~n-jjyGqVnW4uoIrsg$S!gc&l5MIrJyrBrYw9&GD3dWki> z5MCD`ITD=jBYTHeKFiEbtz0Be#xYc8ia)B&xc%L&CF%SThe_6p3**AQPK2VerJIqj zgwH`szV~VpkDD>A8=|LKFSfG1e4XCX(`100GdVVY+}f~^Rj0NeD2b@cg!fTF8iy*w zOssM16|E^GMg>eKk8GCz%EOlj6Ah)G4YI%$u62jz8I!hW<+B#7eSmk2vf_V^y94iG zvJ?Yf5FP#fdtf=DE0XO%{5BDMi^$>ErPVKJEX{^D|NKipy7aXZG7>?`F~D=uXJDtV#mpS8U2c;SvH3BI$nGg#R^& zOPv%5Jwj_}!1(78mlgwhmK z{ZhC1RQC$dmz(O{1xlny_1}_aT70Kg$4P1ILP-`{ z$G#{<=7fm`1$E_QGp&vGKYBbbk72UNH*hys{HurOcy<1;7Jp3GbBnTnnFYw+r2&V=+nlo3 zk_c+Cg~ZUJ8RyTBkByWIOx&K^8WY+xEhGVctv03B1EcQy-#ab>rpO*~(|9-h(3Z_t z;I-_RrL0@n%H;_(mjt%}en}@o@|Uj6+9<;5T$(#v082Y6?biHWVt4uar0~Upk3`nU z@lLs@y}6XNvD!mh^8?>?*GO{cgY6tzhE49i%q*F5%ny7h`nL`_>-x16FVn$NOG*1X z&yu=&QslkR&gPm5XFq()C=urRibr`N7c71GpzNL8i?4##0VChOv1RT{S=>OAsL_w* zI_|wY2JR@XMYn)DLxq?t0^#TcDE7!&w4lb&clIY5$A_0OlDK_HHJhs5Pg*SATSSa# zo z3@Ue25rEMlzL^40sQNdv?}>DM@lqed!HKhZ2o0Cx%U+c=i$9y+s1Am63}XOWLvW-{ zlI!!@{#1}jzkP4<*7`#rCX~H`E_`L+1=ad-+!KEIyIF5x0tzOO!FA1grM(!nR?Ji* zI-2^)wCXm=r9kU^+&;BOgt79n6;W~XT9KGJnhkjOzj)S4xBYLacD+1Q?Xzefq{gKh zAF#>Qa_gFn!m#*L=r6a#Z+_>g;~q&vQaU;`0c8!3(Q^jxc2+V(7XY@|V7{pyqS%@= zxj~>L3!3XibEqx4u4j(>$(F0M^(L45?`g>OB-XX0b#$?K>tOwa39r#^`|# z4C~_+eScS7C_rA|<@=j}(5UgVl*SE~prQyPRf&WG37{3*^QiV3KV$Aq*A|#@HLGv; z*0Dy7*5Rrf>T(n0;bA^CTNj*9?Dbp18Uj@|K-~A#{ojk;E|}qGe-f=?KQSN6Xe%;_Iz`ORP}AdSIwkRCaB}h7B|y0eJjHq%_O=@P!qWdK(C}+ zxokAOWFA%u5Uf<20z|6>x=erRmHvfbRnc5OX0kHsoi`Ak=ri{{`ID?qKH%Of;f~6H zXKsB-`!2`9w-^Adt=!{`J1-h{@KnBllUG#!$oE|TI%kuneu{w&hYQaWrsbrBmvQ-2 z5_0|hl@C=E{nzItT=k1A)t#J*iodcG&cV)*v-GNLfir#C;4DOf+HV~w4%9THo)sxEeQz2 z@|d6%g`lM8`56$~m-qJpFXUj8?l^pw!Jx`WCg`SCu!QN053uD8gbkN+oIz$A${4xN zKEnF$`Ub%hRM`xnJoYq2{+;PB{>4jB!PzK4M0lRfq!O@4P)p6j$cvTrtJws#uLf75 z%4;|WPfNHblKx~bavYXU7v^ZF)EBjCS7Q;|`eVjvkUoop!tQTW;97EJ^^~@Ie7qWX zBGFG<>wbWB8`?S-8?Fc0!(nwB_jiLUH-qwkmMD;!)l%DGF_D5=sBf_jiGdV zjoyKl4<}F3xB$;Wf`mHsaA)aNDcAmT9vrsV2RU6rc>p!W{R=5+{>(BB_l-nL{$Z&3 zKiD|RY1|yCr#i!lP2~?{b!t1Rxhd^j{=24m zZCo1RgQWEJq4H6R=KDI!x-1HWW#TD-v&UuDT#2!?+vn0IZDXHWj@TUWDhaNn_-D*h z;x5w@q|E#$oU-6Io+&<*)=EYI9VVp=0QBA|od@<;8(=2k@A*IIGORjpIpXqDiS}QqvSsl-hm%wV1K&zp<;P zF0EGD4qN=3%=7CT1qpg8GIuF+&}4iYm;kGy|MkzAC>z7jcu(Iyjt1=K>^fzHd1=uQ zn)9oozrIpCCt`C~9;5IbxH9B&-&wf`xHk3!0MM(O7-@a8{3npzO=*BdMb&8B z6^d*FG&Zf2L-C55{LzvK{2R2a`19{ykN!WWi2ZV!jsvE8Y!zq-)pjWj-yGug!~(kn zo6$D~dMSClei;-LWFaU*NnhT}`S0c@$UaNvRJJ4TX07FTW2Siy`r?Gnv8|TUIlU7j zeia(V(KJJWL5KI(SRB_r$`c~ZpbGlA@l-h;c|&{s+RsmR-49be;zGvVdVSqDq9K_& zif`LId5TkxTv&}uJ#E$rb#@Q-SUbx3KBrWCEcW`vKW&mGa{2e2 z{yYrVz~R<&K}}{IN4n{NOWEhj$v#Js2WG1SYqidleq|{SeFbV&J7c9brEZQ=R*X0N z$2R_-Kj_cFmZ)|n{QSu>;UqAQqt;b%X}8=K+@7K+60k>HpAGD?o~!<2Tuu2%cFXra z{xtO6{cVST8anV3;Rg>yTk#2MHnMep{Sq59Mq)F0{N{ zuQ40D3LmUmo3&t&mW@f;+K=$ud9Bwtl)!PySZ4D(XljkaDaKpDe>Aiskr!A`*)xH% zCv@GcHRWFevje409ig!W#I|y@v`j$uo zoS5Va>>vc=;I=t<@(ft~GWA1J_t{^IUqPiYxDIA`h#2It?QOtbJy`wWvsP+RBPoJ0{a8)SjQ}Qi{txdBW7>O;|Mq>N*1-OFlaH>S+U2l7axyV2CqO} zyZ8O8rw&XuZf(Iu_NH|Z5%#h*-d`+}=Epm@Wju6Z7GyDC+cmS*n9Wu2T==0<*=|!{ z#Wg_^Qjxs9nkT*A3QaR`Bi%UIRC|b9bShxb3w?f*Kk!R z-9E1w{?*sUSw#&4Xo5-Ang~Z^uik;|Ajd&XoG0Pnm8a=6^>kLDB&5>q!7zG*-?95( zCw2r_zrpMAz`~UU;k(G6-oGc|TZ`|Vz2&W%3>S;Iy<2eVyCLL9Z7j0FTQ!M`)@D)V zEJ~VmgAj+9GDIiy0M4x3!=5i^gEtvrNz0g@}r3qC!<3>2THd5pT`| z91gCI5jh?4WWdo%InJ!GgKl@!-&_Tic3=#S%HLnYdJ_7z6D7op>(DrL(&wFyCb_4B zxxk&~nKAfTF9x3zh&U zgos(;B#l)Z5G0khYuk22MMs|yyq3m0TH0KsJ0`G^SfKr6>0-hvC_g$L6lv=%aPY%A z41{bDh?+^j#y#0ow$`uGKw+kF*q>vL1jY<{E6D=BuFZLeeXSumD)8c3?^)4u>x_>d zHPx&$`Xn^JC%O7-^)*bD7Tm%boc(Z2l5SY8qabZ6YDqh1(r7DU;R!qq;P=BC?D>ElDJG2T?5*W640&}+L}?TvVc2kqSmAJ^?$ zfpODF?{1B{`RBd%o?)8@`aY#GZX6`&_}IX6gNnxMq8L>5^RJbRcQ&sh-tN#+QgP!4 zB(r&?Ezx&HGV*taR{u$A_CbtxJaxPOIEwM@hlXKHUgwl(SfVKBpd5?|H%z=`AnX|K z;aXxqNc6dnaCNM@+fB?^JTiIwE#cb_UsJT*9?CP$MVvY(xvb%@3j2(NNaR|OfL~Thm7vg7Rr_$NCwo@W+!tuarr(m z$O37F2b7xraO)?~H31@L{27 z^KtC^32Yi4RR^{8gzz~OvnrmWsZbkJokC%=PyQAnYm23$eZwSaI-x=%Z-Z?T-jlNB zOw;7t?$_3BXyW|KhGpj6CmM%a76NCLdPzp{tz!Z7Z>j;Ov*e*j%MkbHJ$Z|uH#(I1 z2SqEDoKqdutLRf|XU|K}MCM;(*@I!(lQ<_M{1}B*O0Ic7&*MEOMT<~UOe`&D8YBeS zXySmp9VotF_KKovx;}#2dYgZBF$Eon89$!bDq)KGe2}3aO-B{P;9}p%gtoX=uRCcL z=Uxn5=NtN-Qi)_m%EE4eMNeGHlTIlH9yG2K2b3hS2KwjHDi$GwaQOb;Zl?1t_Nf|0DsYYIPxhn^g(#iX1 z8~q>lq6Y19vL-YAuSWzLkKRM=AWMR;Bn_*nQXA%0oT0i&eA?e4KSO*iGW{8T7bmhya$l;x3yM&tBRc`@C zJ(Bd$9#3`pEjta|$pFe#=Aq5`6Gg_Jj>1^Bo&W&;Vf92~6*w01z1pxSb>!!XfbHGe RfWHiro&Ldo%|5ZG{|4Pc@6G@K literal 0 HcmV?d00001 diff --git a/docs/user/IsabelleTranslation/index.md b/docs/user/IsabelleTranslation/index.md new file mode 100644 index 0000000..b2c9ee2 --- /dev/null +++ b/docs/user/IsabelleTranslation/index.md @@ -0,0 +1,55 @@ +# Isabelle Translation + +-- *Author: Nils Buchholz*, February 2025 valid for a future release of KeY based on KeY 2.12.3 + +!!! abstract + + This note describes the new *Isabelle Translation* extension in KeY 2.12.3 + When enabled it can be used to translate sequents to Isabelle and automatically search for proofs using Isabelle + +## Overview + +The Isabelle Translation plugin provides automated translation of KeY sequents to Isabelle/HOL. It also allows for automated proof search using Isabelle on these translations. +The Isabelle translation can be used on any update-free sequent. Further details on the intricacies of the translation can be found under [https://doi.org/10.5445/IR/1000176239](https://doi.org/10.5445/IR/1000176239). +Thus it is necessary to first remove these from the sequent. This can be done automatically via the SMT Preparation macro in most cases. +The translation is accessible through the context menu of the whole sequent, which can be opened by right-clicking the sequent arrow. There are two options in this menu. + +`Translate to Isabelle` + + >This option translates only the currently selected goal and starts the automated proof search in Isabelle. + +`Translate all goals to Isabelle` + + >This option translates all open goals in the currently selected proof and starts automated proof searches for them. + + +The proof search is currently conducted using "Isabelle sledgehammer", which calls a variety of SMT solvers and ATP provers to conduct its searches. More information about sledgehammer can be found at https://isabelle.in.tum.de/dist/doc/sledgehammer.pdf. + +## Interface +Using the translation opens an interface. This interface will display the status of the Isabelle launch and the individual proof search progress for all translated goals. +The current status is shown in a bar at the top of the interface. This will at first show that the Isabelle is preparing to signify the starting of Isabelle and the creation of the preamble session files. When first starting Isabelle or changing the translation directory this may take up to a few minutes. Afterwards it will display the number of processed goals. +From this interface the proof search can be aborted using the Stop button. After proof sarch completes for all goals the results can be discarded, which closes the interface or applied, which automatically closes the relevant goals with custom rules containing the result of the respective sledgehammer calls. + +
+ ![IsabelleInterface](./IsabelleInterface.png) +
Isabelle Interface during proof search
+
+ +## Setup +The Isabelle Translation can be enabled like all other KeY plugins. +To use the automatic proof search parts of the Isabelle Translation, an Isabelle installation is required. In the plugin settings the path to the Isabelle directory can be configured. The path set here should point to the folder containing the Isabelle executable. + +## Settings + +Currently the Isabelle Translation provides two settings. These are found under Options>Settings>Isabelle Translation. + +`Location for translation files` + >This setting determines where the translation files should be stored. This includes the session files as well as the Isabelle theories for the preamble and the sequent translation. + +`Isabelle installation folder` + >This setting sets the folder of the Isabelle installation, as described in the Setup section. + +`Timeout` + >This setting sets the timeout for proof searches in seconds. + +There is an additional button to check if a given version of Isabelle is supported. Currently the supported versions are Isabelle2023 and Isabelle2024-RC1. \ No newline at end of file From f6c63503573896d662e70268e61c7b6311329c52 Mon Sep 17 00:00:00 2001 From: BookWood Date: Wed, 7 May 2025 12:27:50 +0200 Subject: [PATCH 2/2] add overview of translation structure among other adjustments --- docs/user/IsabelleTranslation/index.md | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/docs/user/IsabelleTranslation/index.md b/docs/user/IsabelleTranslation/index.md index b2c9ee2..6a6a2d6 100644 --- a/docs/user/IsabelleTranslation/index.md +++ b/docs/user/IsabelleTranslation/index.md @@ -9,8 +9,8 @@ ## Overview -The Isabelle Translation plugin provides automated translation of KeY sequents to Isabelle/HOL. It also allows for automated proof search using Isabelle on these translations. -The Isabelle translation can be used on any update-free sequent. Further details on the intricacies of the translation can be found under [https://doi.org/10.5445/IR/1000176239](https://doi.org/10.5445/IR/1000176239). +The Isabelle Translation plugin provides automated translation of KeY sequents to Isabelle/HOL. It also allows for automated proof search using Isabelle on these translations. +The Isabelle translation can be used on any update-free sequent. Thus it is necessary to first remove these from the sequent. This can be done automatically via the SMT Preparation macro in most cases. The translation is accessible through the context menu of the whole sequent, which can be opened by right-clicking the sequent arrow. There are two options in this menu. @@ -36,7 +36,8 @@ From this interface the proof search can be aborted using the Stop button. After ## Setup -The Isabelle Translation can be enabled like all other KeY plugins. + +The Isabelle Translation can be enabled under Options>Settings>Extensions. To use the automatic proof search parts of the Isabelle Translation, an Isabelle installation is required. In the plugin settings the path to the Isabelle directory can be configured. The path set here should point to the folder containing the Isabelle executable. ## Settings @@ -52,4 +53,12 @@ Currently the Isabelle Translation provides two settings. These are found under `Timeout` >This setting sets the timeout for proof searches in seconds. -There is an additional button to check if a given version of Isabelle is supported. Currently the supported versions are Isabelle2023 and Isabelle2024-RC1. \ No newline at end of file +There is an additional button to check if a given version of Isabelle is supported. Currently the supported versions are Isabelle2023 and Isabelle2024-RC1. + + +## Translation Structure +The translation is structured into a preamble file containing the definitions of the JFOL types and their axioms and the main translation file. The translation file contains the definitions of the specific Java class types present on the sequent and their associated functions. The translation file also contains a locale, which contains the antecedents of the sequent and a theorem holding the succedents. The file ends after the theorem declaration. +Further details on the intricacies of the translation can be found under [https://doi.org/10.5445/IR/1000176239](https://doi.org/10.5445/IR/1000176239). + +### Interactive Proving Warning +When opening the translation files for interactive proving in Isabelle, Isabelle must be instructed to include the translation directory as a session directory. This can be done using the "-d" command argument when opening Isabelle. If this is not done, Isabelle will fail to recognize the KeYTranslations session and thus not find the preamble theory. This can also be circumvented by removing the session prefix "KeYTranslations." from the preamble theory import. This will make Isabelle search the local directory for the theory. \ No newline at end of file