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