[isabelle-dev] NEWS

[Makarius]

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