Changeset 1599 for src/common/Floats.ma


Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (10 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/common/Floats.ma

    r961 r1599  
    5959
    6060axiom Fcmp_ne_eq:
    61   ∀ f1,f2. Fcmp Cne f1 f2 = ¬(Fcmp Ceq f1 f2).
     61  ∀ f1,f2. Fcmp Cne f1 f2 = (¬(Fcmp Ceq f1 f2)).
    6262axiom Fcmp_le_lt_eq:
    6363  ∀ f1,f2. Fcmp Cle f1 f2 = (Fcmp Clt f1 f2 ∨ Fcmp Ceq f1 f2).
Note: See TracChangeset for help on using the changeset viewer.