[isabelle] Defining Real numbers axiomatically



Hi,
  Can somebody tell me if there is a way to define the real number type
axiomatically in Isabelle, preferably using IFOL or FOL? I guess what I
basically what I need is a way to define a partial function so that I can
define the properties of say addition without actually implementing
addition.

Thanking in advance,
Sincerely,

 Jyothis V,
 IIT Kharagpur,
 India




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