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