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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
