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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
