[isabelle-dev] Quickcheck_Exhaustive.unknown

[Tobias Nipkow]

Am 30/11/2011 12:27, schrieb Makarius:
> This concerns Isabelle/3d6ee9c7d7ef:
> 
> Adding a global constant Quickcheck_Exhaustive.unknown with rather
> generic notation "?" to main HOL is a bit dangerous.  The name "unknown"
> is also a candidate for "hide_const (open)".

I would like to emphasize this. Local names (i.e. those that the clients
of a package or theory do not need to know) should stay local, i.e.
should be hidden at the end. This is particularly important if the name
is something generic like "Times" or "unknown" that other people may
want to use, too, w/o suffering from long names. Quickcheck is
particularly generous in what it exports...

Tobias

> It appears to be used only for output anyway, so the syntax can be
> easily attached to the local context before printing.
> 
> There are more ways to do it, if slightly different functionality is
> required.  E.g. see the more advanced Proof_Syntax.proof_syntax or
> Nitpick_Model.add_wacky_syntax, although this is heavy gear.
> 
> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev