[isabelle-dev] Towards the next release

[Florian Haftmann]

Am 22.03.2012 11:42, schrieb Makarius:
> On Fri, 16 Mar 2012, Florian Haftmann wrote:
> 
>> * 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.

> Does it mean both will reforms will be finished for the coming release?

The plan is to do so, until the end of April.

The numeral story is invasive at the foundations of arithmetic, but much
less in user space since users seldomly tinker around with internal
numeral representations (HOL-Word being a notable exception).  With a
release envisaged for the mid of the year, two months after remerging
that fork seems appropriate.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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/20120322/6a21dd3c/attachment.sig>