*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Finding the instantiation of a variable*From*: Makarius <makarius at sketis.net>*Date*: Mon, 26 Jul 2010 21:26:01 +0200 (CEST)*In-reply-to*: <4C437137.4090502@in.tum.de>*References*: <AANLkTinrTaBPr1dIqPvVJgyJOBL92-jnc7TRXA_1wFYg@mail.gmail.com> <AANLkTimZ9yLWnR7XFXoAzNKmkHvn0bSOvd_XKT-J4qtW@mail.gmail.com> <4C3B1DE6.4040305@in.tum.de> <AANLkTimT1qdp2v436l9VmLeGGZKZgfnmJvfuB0SevMd0@mail.gmail.com> <4C437137.4090502@in.tum.de>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Sun, 18 Jul 2010, Alexander Krauss wrote:

I've tried running 'full_prf' after 'apply auto', but I get an errorabout 'minimal proof object' even I have Full Proof switched on in PG.I am surprised by this myself. I would also have expected a full proofhere. Maybe someone else has an idea?

Makarius

**References**:**[isabelle] Finding the instantiation of a variable***From:*Steve W

**Re: [isabelle] Finding the instantiation of a variable***From:*Steve W

**Re: [isabelle] Finding the instantiation of a variable***From:*Alexander Krauss

**Re: [isabelle] Finding the instantiation of a variable***From:*Steve W

**Re: [isabelle] Finding the instantiation of a variable***From:*Alexander Krauss

- Previous by Date: [isabelle] Mutually recursive coinductive predicates
- Next by Date: Re: [isabelle] Mutually recursive coinductive predicates
- Previous by Thread: Re: [isabelle] Finding the instantiation of a variable
- Next by Thread: [isabelle] locales and 'types'
- Cl-isabelle-users July 2010 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