[isabelle-dev] Quickcheck_Exhaustive.unknown

[Makarius]

On Wed, 30 Nov 2011, Makarius wrote:

> 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)".
>
> 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.

Yet another possibility:

   axiomatization unknown :: 'a

   notation (output) unknown  ("?")

Here 'axiomatization' prevents later definition of that unknown thing.
The output notation prevents pollution of global input grammar.


 	Makarius