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 http://isabelle.in.tum.de/~haftmann/misc/screencast/big_operators.mp2t 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. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
