[isabelle-dev] Quickcheck_Exhaustive.unknown

[Lukas Bulwahn]

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 still argue that anyway
> find_theorems etc. should ignore everything which cannot by access by
> name through the name space.
>
I was expecting that *names* hidden with hide_fact do not effect 
find_theorems -- even though it is quite arguably why the artefacts 
should be found after that operation.

But I am surprised that the Binding.conceal in ML does not have any 
effect either.

Lukas