[isabelle-dev] Quickcheck_Exhaustive.unknown

[Lukas Bulwahn]

On 11/30/2011 01:14 PM, Makarius wrote:
> 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.
>
>

Changeset 3b7c35a08723 follows your suggestion. Thanks for these hints.


Lukas