Am 30/11/2011 12:27, schrieb Makarius: > 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)".
I would like to emphasize this. Local names (i.e. those that the clients of a package or theory do not need to know) should stay local, i.e. should be hidden at the end. This is particularly important if the name is something generic like "Times" or "unknown" that other people may want to use, too, w/o suffering from long names. Quickcheck is particularly generous in what it exports... Tobias > 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. > > > Makarius > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev