On Fri, Oct 5, 2012 at 10:37 AM, Makarius <makar...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev