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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
