[isabelle-dev] typedef (open) legacy

[Makarius]

On Thu, 4 Oct 2012, Brian Huffman wrote:

> I was reluctant to support "closed" type definitions at all in HOLCF's 
> cpodef and friends, preferring to make (open) the default behavior; but 
> in the end I decided it was more important to make the input syntax 
> consistent with typedef. I would be more than happy to remove this 
> feature from the HOLCF packages if typedef will be changed to match.

Do you want to make the first move to remove the (open) option from the 
HOLCF cpodef packages?  I will later follow trimming down HOL typedef -- 
there are a few more fine points on my list to iron out there once the set 
defs are gone. Alternatively, I can take do it for 'typdef' packages 
simultaneously.

Before doing anything on the packages, we should make another round 
through the visible universe of theories to eliminate the last uses of the 
legacy mode.


 	Makarius