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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
