Hi *, I am currently busy with stocktaking the results of my visit to TUM last Wednesday, and I have updated the current state of two affairs in the wiki:
* The set story: https://isabelle.in.tum.de/community/Having_%27a_set_back Not everything mentioned there is an ultimate need, but we should strive to pick as many fruits as we can from the set type constructor – the more likely this will compensate users if they have to adjust their theories * The numeral story: https://isabelle.in.tum.de/community/Numerals It looks quite good (preliminary tests of the AFP did not reveal much problems). The fork should be done by the end of April. The further perspectives listed there are no need-to-haves for the next release. I further did some doodling around with mira; after 14 staying away from there I did not encountered fundamental difficulties, but my original intent, operative configurations for distribution build and docs, did not grow very far. I will set aside this as it is by now and would appreciate if anybody would continue on this, sooner or later. After this experience I will keep mira on my screen, but when I will return to it I plan to focus on * re-learn what the current deployment at TUM is * improve the notoriously annoying settings mechanisms * minor technical improvements before doing anything end-user visible. Cheers, 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
