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

[Andreas Schropp]

On 08/24/2011 08:30 PM, Florian Haftmann wrote:
>> I don't think it's possible to have it both ways. We need to either say we are making this change (and then pushing it through) or not making this change.
>>      
> Having full compatible versions indeed is illusive.

Why exactly?

 From a naive POV sets and predicates are isomorphic and
results about them could be transferred at any time.
Not that I advocate this on a large scale, but where does
this break down? Tools?
Is this intrinsic or rather an artifact of Isabelle or HOL?

I am asking because I still believe that one day
(somewhat distant, even given my levels of optimism ^^)
theorem proving will be modulo isomorphisms.
I.e. Voevodsky et. al.'s vision should become true not only
in the fancyful calculi they are designing.

Cheers,
   Andy