bulwahn at in.tum.de
Fri Dec 9 16:48:12 CET 2011
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
More information about the isabelle-dev