*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] A small proof checker (String => Bool)*From*: Mark Adams <mark at proof-technologies.com>*Date*: Mon, 28 Oct 2019 19:08:20 +0000*Cc*: isabelle-users at cl.cam.ac.uk, Juho Kupiainen <juho.kupiainen.general.ai.group at gmail.com>*In-reply-to*: <c023779c-0068-c89c-5a29-6d807c97f9de@sketis.net>*References*: <CADnKKmJX6c2SK-aOTm6aLYMMyjk94U+0_btp1HTEth4ENpozBw@mail.gmail.com> <c023779c-0068-c89c-5a29-6d807c97f9de@sketis.net>*User-agent*: Roundcube Webmail/1.3.7

Hi Juho,

Mark. On 26/10/2019 11:22, Makarius wrote:

On 25/10/2019 17:07, Juho Kupiainen wrote:How could I go about obtaining a small proof checker for Isabelle HOL,thattakes a theory file and checks that it's valid? I would like it to besimple to understand and as few lines of code as possible, yet itshouldinclude the axioms of the system and be able to check the wholearchive offormal proofs.It sound like you ask for an "uninformative green light" for your theories, but that is neither realistic nor useful. You need to be more specific about what you mean, and what the application actually context is. So many things can go wrong. You need to think about what you want to get right in which way. Makarius

**Follow-Ups**:**Re: [isabelle] A small proof checker (String => Bool)***From:*mukesh tiwari

**References**:**[isabelle] A small proof checker (String => Bool)***From:*Juho Kupiainen

**Re: [isabelle] A small proof checker (String => Bool)***From:*Makarius

- Previous by Date: Re: [isabelle] (Super-)Martingale and conditional expectation
- Next by Date: Re: [isabelle] A small proof checker (String => Bool)
- Previous by Thread: Re: [isabelle] A small proof checker (String => Bool)
- Next by Thread: Re: [isabelle] A small proof checker (String => Bool)
- Cl-isabelle-users October 2019 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