> 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.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
