[isabelle-dev] typedef (open) legacy

[Brian Huffman]

On Fri, Oct 5, 2012 at 10:37 AM, Makarius <makarius at sketis.net> wrote:
> 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.

Hi Makarius,

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?

- Brian

>
> 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