Ignore:
Timestamp:
Nov 26, 2010, 3:33:32 PM (10 years ago)
Author:
mulligan
Message:

Added axioms for addition for claudio.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Arithmetic.ma

    r286 r313  
    2828ndefinition nineteen ≝ ten + nine.
    2929ndefinition twenty_four ≝ sixteen + eight.
     30ndefinition thirty_two ≝ sixteen + sixteen.
    3031ndefinition one_hundred ≝ ten * ten.
    3132ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
Note: See TracChangeset for help on using the changeset viewer.