[isabelle-dev] NEWS

[Lawrence Paulson]

It seems to me that we owe users an announcement on the mailing list so that they know that this is coming. They can then download a development snapshot to see what it will look like.
Larry

On 4 Jan 2012, at 21:10, Makarius wrote:

> On Wed, 4 Jan 2012, Lawrence Paulson wrote:
> 
>> I did quite a few of these conversions. Generally the changes were straightforward, EXCEPT for theories that explicitly treated sets as predicates. In the former case, the strategy is to rigorously confine yourself to set primitives, but in the latter case, you may find yourself with a colossal mess.
> 
>> On 4 Jan 2012, at 20:18, Florian Haftmann wrote:
>>> Good question how such explicit instructions could look like.
>>> Eliminating mem_def/Collect_def in a first pass is usually not feasible,
>>> because the set/pred-ignorant versions of Isabelle tended to move back
>>> and forth between both worlds by their automation setup.  The migration
>>> strategy had always been to adjust terms to respect the set/pred
>>> distinction, and then adjust the proofs accordingly.  No trick behind it.
> 
> A good NEWS entry just rephrases the experience of your own porting into one well-written paragraph.  There are no tricks once you know how to do it.
> 
> I am used to apply prospective changes mentally to every theory of other users that I happen to see.  From what I've seen in the past few months, the 'a set reconversion is likely to break a lot of things out there, so users need to do this the proper way from the start. (Often users just hold their breath and jump right into a new version, even more than one step in the chain of official releases.)
> 
> 
> 	Makarius