*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Verify the legitimacy of a proof?*From*: scott constable <sdconsta at syr.edu>*Date*: Fri, 7 Jul 2017 09:37:14 -0700

Hi All, Let's suppose I have some lemma lemma ComplexProperty: "something interesting" ... done whose proof cites numerous other lemmas in other .thy files, possibly written by other persons with malicious intentions. Is there a command in Isabelle which I could use to determine the legitimacy of the entire proof tree of ComplexProperty? That is, I want to ensure that no lemma in the proof tree ended with "sorry", or if any axioms were used, I want to know which ones, etc. Thanks, Scott Constable

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

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

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

- Previous by Date: [isabelle] New AFP entry: CRDT
- Next by Date: Re: [isabelle] Verify the legitimacy of a proof?
- Previous by Thread: [isabelle] New AFP entry: CRDT
- 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