*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Verify the legitimacy of a proof?*From*: Mark Adams <mark at proof-technologies.com>*Date*: Sat, 08 Jul 2017 19:43:40 +0200*Cc*: isabelle-users at cl.cam.ac.uk, scott constable <sdconsta at syr.edu>*In-reply-to*: <d48e07ee-6071-cbd1-c4cf-38eead2edfb3@sketis.net>*References*: <CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw@mail.gmail.com> <d48e07ee-6071-cbd1-c4cf-38eead2edfb3@sketis.net>*User-agent*: Roundcube Webmail/1.2.1

On 08/07/2017 12:46, Makarius wrote:

HOL-Zero is a notable exception in targeting a market of potentially malicious (ab-)users, but it is not a "big prover".

Mark.

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

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

- 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