<div dir="ltr"><br>Sending the message again (image attachments are not allowed in this list so it was held for moderator<div>approval). With respect to the keyboard model,<div>I have a standard (<span class="" style>samsung</span>) PS/2 keyboard.</div>
<div><br></div><div>Related to the sidekick pane mention below, instead of the operator symbols, the pane shows (empty) boxes.<br></div><div><br></div><div>Cheers<br><div class="gmail_quote">---------- Forwarded message ----------<br>
From: <b class="gmail_sendername"><span class="" style>Alfio</span> Martini</b> <span dir="ltr"><<a href="mailto:alfio.martini@acm.org" target="_blank"><span class="" style>alfio</span>.martini@<span class="" style>acm</span>.org</a>></span><br>

Date: Tue, Sep 10, 2013 at 12:53 PM<br>Subject: Isabelle-10-Sept<br>To: <a href="mailto:isabelle-dev@mailbroy.informatik.tu-muenchen.de" target="_blank"><span class="" style>isabelle</span>-<span class="" style>dev</span>@<span class="" style>mailbroy</span>.<span class="" style>informatik</span>.<span class="" style>tu</span>-<span class="" style>muenchen</span>.<span class="" style>de</span></a><br>
<br><br><div dir="ltr">Hi,<div>
<br></div><div>I will start his thread. First of all, it is a  very nice addition this pane </div><div>that allows direct access to documentation. Also, PG fans will welcome the</div><div>auto_solve feature which detects if the conjecture as an immediate proof</div>


<div>by some other fact in the current theory or somewhere else in Main. </div><div>Thanks a lot.</div><div><br></div><div>On the other hand, the (propositional) operators of <span class="" style>HOL</span>-formulae are still not properly</div>
<div>

shown in the sidekick pane as the image attached shows. I am not</div><div>sure if this is a "feature" or a known bug, but this is problem is</div><div>also present in</div><div>the current version.</div><div><br>


</div><div>Also, <span class="" style>numpad</span> doesn´t work at all (as already pointed out). I am using</div><div>an Windows 8 machine.</div><div><br></div><div>Cheers</div><span><font color="#888888"><div><div><br>
</div>-- <br>
<div dir="ltr"><span class="" style>Alfio</span> Ricardo Martini<br>PhD in Computer Science (TU Berlin)<div>
<a href="http://www.inf.pucrs.br/alfio" target="_blank">www.inf.<span class="" style>pucrs</span>.<span class="" style>br</span>/<span class="" style>alfio</span></a><br><div>Lattes:  <a href="http://lattes.cnpq.br/4016080665372277" target="_blank">http://lattes.<span class="" style>cnpq</span>.<span class="" style>br</span>/4016080665372277</a><br>
Associate Professor at Faculty of Informatics (<span class="" style>PUCRS</span>)<div>

Av. <span class="" style>Ipiranga</span>, 6681 - <span class="" style>Prédio</span> 32 - <span class="" style>Faculdade</span> <span class="" style>de</span> <span class="" style>Informática</span></div><div>90619-900 -Porto <span class="" style>Alegre</span> - RS - <span class="" style>Brasil</span></div>
</div></div></div>
</div></font></span></div>
</div><br><br clear="all"><div><br></div>-- <br><div dir="ltr"><span class="" style>Alfio</span> Ricardo Martini<br>PhD in Computer Science (TU Berlin)<div><a href="http://www.inf.pucrs.br/alfio" target="_blank">www.inf.<span class="" style>pucrs</span>.<span class="" style>br</span>/<span class="" style>alfio</span></a><br>
<div>Lattes:  <a href="http://lattes.cnpq.br/4016080665372277" target="_blank">http://lattes.<span class="" style>cnpq</span>.<span class="" style>br</span>/4016080665372277</a><br>
Associate Professor at Faculty of Informatics (<span class="" style>PUCRS</span>)<div>Av. <span class="" style>Ipiranga</span>, 6681 - <span class="" style>Prédio</span> 32 - <span class="" style>Faculdade</span> <span class="" style>de</span> <span class="" style>Informática</span></div>
<div>90619-900 -Porto <span class="" style>Alegre</span> - RS - <span class="" style>Brasil</span></div></div></div></div>
</div></div></div>