[isabelle-dev] Quickcheck_Exhaustive.unknown

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Dec 9 16:41:58 CET 2011

> 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.




PGP available:

More information about the isabelle-dev mailing list