[isabelle-dev] Release reminder

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Aug 25 21:32:02 CEST 2011

>> Since August is the canonical time for vacation for many people it is
>> probably better to get into more concrete discussions in 3-4 weeks from
>> now, but people can already start thinking about their own areas of
>> responsibility concerning consolidation for the release.

I have two topics on the screen
* Complete_Lattice.thy
  * eliminate some historical legacy theorems (Johannes Hölzl and me)
  * further default simp rules (Lars Noschinski and me)
* Separating predicates and sets syntactically

Details of the last point can be followed on the mailing list
conversations.  As already proposed, I would refrain from such
fundamental changes like introduction a set type constructor before that




PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110825/00ebcad1/attachment.sig>

More information about the isabelle-dev mailing list