[isabelle-dev] Isabelle-10-Sept

[Alfio Martini]

Hi,

I will start his thread. First of all, it is a  very nice addition this
pane
that allows direct access to documentation. Also, PG fans will welcome the
auto_solve feature which detects if the conjecture as an immediate proof
by some other fact in the current theory or somewhere else in Main.
Thanks a lot.

On the other hand, the (propositional) operators of HOL-formulae are still
not properly
shown in the sidekick pane as the image attached shows. I am not
sure if this is a "feature" or a known bug, but this is problem is
also present in
the current version.

Also, numpad doesn´t work at all (as already pointed out). I am using
an Windows 8 machine.

Cheers

-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
www.inf.pucrs.br/alfio
Lattes:  http://lattes.cnpq.br/4016080665372277
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130910/092d6d0e/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: sidekick-op.PNG
Type: image/png
Size: 113282 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130910/092d6d0e/attachment-0001.png>