On Thu, 4 Oct 2012, Florian Haftmann wrote:
I think either option 3 or 4 would make sense, although I'd say 4 is
preferable for a couple of reasons: First, it makes the implementation
of typedef simpler. Second, it actually gives users more flexibility
because if they want a set constant, they can use any definition
package, not just "definition". The extra verbosity in some cases is a
small price to pay.
I would support (4). In the long run, typedef should be the bare
foundational minimum for introducing HOL types
I also remember it like that -- most package authors were already in
favour of (4) "open only without option" some years ago, but we never made
the move.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
