Re: [isabelle] Defining Real numbers axiomatically
> tell me if there is a way to define the
> real number type
> axiomatically in Isabelle, preferably using IFOL or FOL?
In Isabelle/ZF you can do it as in IsarMathLib's OrderedField_ZF theory,
see section "Definition of real numbers" at the end of
It is not a type then of course but a quadruple of sets.
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)
This archive was generated by a fusion of
Pipermail (Mailman edition) and