On 08/07/2017 13:30, Makarius wrote:
On 08/07/17 13:01, Manuel Eberl wrote:Unfortunately, it is very easy to circumvent this. I don't recall who found this originally, but you can hide the âtaintâ of a theorem by going through a type class instantiation:"Found this originally" sounds very funny to me. Of course, the problem of oracles vs. type classes instantiations is as old as oracles and type class instantiations in Isabelle. It is rather well-known for insiders.
I am sure Manuel meant no disrespect. No doubt you were aware of this behaviour from the start.
It is usually due to a fanciful interpretation of the documentation. The latter says that "The system always records oracle invocations within derivations of theorems by a unique tag." but does not claim that these tags are also always inherited in the way one is all too likely to assume. There you are, Manuel.So we are back to the new meta-problem from recent years: even power users don't know anymore what Isabelle is and what it does, and especially what it does not.
Description: S/MIME Cryptographic Signature