makarius at sketis.net
Wed Nov 30 13:14:27 CET 2011
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.
More information about the isabelle-dev