*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Reading a proof*From*: Makarius <makarius at sketis.net>*Date*: Fri, 30 Sep 2011 18:29:15 +0200 (CEST)*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAP0k5J6Pf-N_6+He_MJzQPBZNb+Uf5uv8rWYq0b64U0tcpKB5w@mail.gmail.com>*References*: <CAP0k5J6Pf-N_6+He_MJzQPBZNb+Uf5uv8rWYq0b64U0tcpKB5w@mail.gmail.com>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Fri, 30 Sep 2011, John Munroe wrote:

Suppose I have the following: axiomatization f :: "nat => nat" where ax: "f 0 = 0" lemma "f 0 = 0 | f 0 = 1" using ax apply auto done Clearly, auto finds a proof because the first disjunct can be inferred. I'm trying to dig into the proof and see which disjunct is actually proved by auto (or simp, when appropriate). I've tried switching on 'Full Proof' from the Isabelle menu in PG and sticking 'full_prf' after 'apply auto', but I get an error saying "reconstruct_proof: minimal proof object'. Is there a way to see which disjunct is proved in either Isar or ML level? Could one see which disjunct is proved by looking at the proof term? How to retrieve the proof term?

Isabelle2011/build -m HOL-Proofs This logic image then needs to be selected in PG when starting up. Makarius

**Follow-Ups**:**Re: [isabelle] Reading a proof***From:*John Munroe

**References**:**[isabelle] Reading a proof***From:*John Munroe

- Previous by Date: Re: [isabelle] term notation affects type parsing
- Next by Date: Re: [isabelle] Reading a proof
- Previous by Thread: [isabelle] Reading a proof
- Next by Thread: Re: [isabelle] Reading a proof
- Cl-isabelle-users September 2011 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