[isabelle-dev] typedef (open) legacy

[Makarius]

On Thu, 4 Oct 2012, Florian Haftmann wrote:

>> I think either option 3 or 4 would make sense, although I'd say 4 is
>> preferable for a couple of reasons: First, it makes the implementation
>> of typedef simpler. Second, it actually gives users more flexibility
>> because if they want a set constant, they can use any definition
>> package, not just "definition". The extra verbosity in some cases is a
>> small price to pay.
>
> I would support (4).  In the long run, typedef should be the bare 
> foundational minimum for introducing HOL types

I also remember it like that -- most package authors were already in 
favour of (4) "open only without option" some years ago, but we never made 
the move.


 	Makarius