*To*: Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem*From*: Makarius <makarius at sketis.net>*Date*: Fri, 20 Jul 2012 16:34:28 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5009674D.9070804@gmx.com>*References*: <5008228D.9070306@gmx.com> <500827AE.6020907@gmx.com> <50087706.2030608@gmx.com> <alpine.LNX.2.00.1207201318440.20336@macbroy21.informatik.tu-muenchen.de> <5009674D.9070804@gmx.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 20 Jul 2012, Gottfried Barrow wrote:

Quantifying over functions has me a little worried.

Makarius

**Follow-Ups**:**Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem***From:*Gottfried Barrow

**References**:**[isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem***From:*Gottfried Barrow

**Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem***From:*Gottfried Barrow

**Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem***From:*Gottfried Barrow

**Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem***From:*Makarius

**Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] provers used by sledgehammer
- Next by Date: Re: [isabelle] provers used by sledgehammer
- Previous by Thread: Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem
- Next by Thread: Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem
- Cl-isabelle-users July 2012 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