On 12/09/2011 04:41 PM, Florian Haftmann wrote:
Unfortunately, the find_theorems command is quite ignorant to any means
to hide facts:
Facts that have been hidden, can be found.
Note that with »hide« you do *not* hide the artefacts, but their name
access. The artefacts are still there. You can
> Unfortunately, the find_theorems command is quite ignorant to any means
> to hide facts:
> Facts that have been hidden, can be found.
Note that with »hide« you do *not* hide the artefacts, but their name
access. The artefacts are still there. You can still argue that anyway
find_theorems etc.
On 11/30/2011 03:17 PM, Tobias Nipkow wrote:
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_cons
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
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 (o
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 o
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 easi
