[isabelle-dev] typedef (open) legacy

[Makarius]

On Mon, 8 Oct 2012, Brian Huffman wrote:

> I have a changeset that removes the set-definition features from the
> {cpo,pcpo,domain}def commands in HOLCF, and it checks successfully on
> testboard.
>
> http://isabelle.in.tum.de/testboard/Isabelle/rev/a093798fa71b
>
> Should I go ahead and push this changeset to the current tip?

I cannot connect to testboard at the moment, it seems to be in bad shape 
again.

If the above is a more or less standard change to the packages and 
libraries to remove the (open) option, please go ahead and push it.  I 
will join in a bit later to follow up with some further tuning, and remove 
the last traces of the set defs from the HOL typedef package 
implementation.

If it is more complex and needs some further discussion, we can also do it 
via some clone on bitbucket or elsewhere, e.g. see my 
https://bitbucket.org/makarius/isabelle, although I don't expect any 
difficulties for such a routine thing here.


 	Makarius