[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Makarius]

On Fri, 12 Aug 2011, Alexander Krauss wrote:

> Instead of stating an opinion, let me recall the parts of the story so 
> far that I know, to avoid that history repeats itself. I am sure that 
> Stefan will add some interesting details, too. (He wrote to me that it 
> may take him a few days to comment on this thread.)
>
> 2007
> 2008

Thanks for digging up the history, it sheds some further light on it.

I abstain from voicing an oponion on the matter itself, because I am not 
an expert of the increasingly complex Isabelle/HOL library.  In 2008 I've 
lost some nice Isar proofs due to change of the HO unification behaviour, 
but that was only a minor disadvantage, and predicates are nicer in many 
situations, which does not mean there could not be a separate set type, 
even though Coq and HOLs prefer predicates.


I am more concerned about the general process of such upheavals, and hope 
that more time is taken this time to consider the moves.  In particular we 
are already a bit late in the release schedule, and things are supposed to 
converge soon. So anything that cannot be finished within very few weeks 
needs to be postponed. (People who have participated in the 2006/2007 
release desaster know what I mean.)


 	Makarius