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

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

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

I know that "=" as axiomatized in HOL.thy is a HOL function as introduced on line 98: eq :: "['a, 'a] => bool".

I naively adopt the logical symbols /\, \/, -->, ~, =, \<forall>, \<exists>, and <-> as my FOL logical symbols.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.