[isabelle-dev] Big Operators

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Apr 11 11:47:50 CEST 2013

There is a record of a rough talk I gave recently concerning Big
Operators.  It might be of interest for a wider audience.

Please note that it is really rough, with the audience sometimes
assisting me to present things the most comfortable way nowadays in
jedit ;-).

The record of the presentation (thanks Johannes) can be found at


There are a few caveats:
* The web server does not seem to deliver the correct MIME type; save it
locally at a glance and open it there.
* The file is extensively big.  I did not manage to compress it because
the whiteboard notes become unreadable then

Overall, I still like that idea but will investigate alternative
technologies in the future.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130411/417ceccb/attachment.asc>

More information about the isabelle-dev mailing list