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