*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Thu, 19 Jul 2012 10:28:46 -0500*In-reply-to*: <5008228D.9070306@gmx.com>*References*: <5008228D.9070306@gmx.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 7/19/2012 10:06 AM, Gottfried Barrow wrote:

Alright, but with Isabelle, I can never be so minimalist. Myminimalist logic on top of HOL needs a declared type, and the "=" isgiven as the FOL logical symbol which is (partly or fully) axiomatizedby four axioms starting at line 196 of src/HOL/HOL.thy. I understandthe first 2 axioms, but not the second 2.

Regards, GB

**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

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