[isabelle-dev] typedef (open) legacy

Makarius makarius at sketis.net
Tue Oct 9 11:20:22 CEST 2012

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 

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 

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.


More information about the isabelle-dev mailing list