*To*: Manuel Eberl <eberlm at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Verify the legitimacy of a proof?*From*: Makarius <makarius at sketis.net>*Date*: Sat, 8 Jul 2017 13:30:43 +0200*In-reply-to*: <17fc53a1-ef75-ac0b-4e7b-0a9dca6fa918@in.tum.de>*References*: <CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw@mail.gmail.com> <CAGbqCMxFwASJH4ympZ589fVua9-kX0qs4K-HAb1z5XgSPg2=Bw@mail.gmail.com> <CAASQnwOXcZsZJ4YyoTUDXxTeZHXbLoic=fhJ5XmmE9Gv9eWmvw@mail.gmail.com> <17fc53a1-ef75-ac0b-4e7b-0a9dca6fa918@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.1.1

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

**Follow-Ups**:**Re: [isabelle] Verify the legitimacy of a proof?***From:*Tobias Nipkow

**References**:**[isabelle] Verify the legitimacy of a proof?***From:*scott constable

**Re: [isabelle] Verify the legitimacy of a proof?***From:*C. Diekmann

**Re: [isabelle] Verify the legitimacy of a proof?***From:*Simon Wimmer

**Re: [isabelle] Verify the legitimacy of a proof?***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Date: Re: [isabelle] Verify the legitimacy of a proof?
- Previous by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Cl-isabelle-users July 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list