[isabelle-dev] Quickcheck_Exhaustive.unknown

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

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