Ignore:
Timestamp:
Nov 24, 2010, 6:29:12 PM (10 years ago)
Author:
mulligan
Message:

Resolved conflicts.

File:
1 edited

Legend:

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

    r277 r281  
    2727ndefinition eighteen ≝ nine + nine.
    2828ndefinition nineteen ≝ ten + nine.
     29ndefinition one_hundred ≝ ten * ten.
    2930ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
     31ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one.
     32ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one.
     33ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one.
     34ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven.
     35ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one.
     36ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one.
     37ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten.
     38ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one.
     39ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one.
     40ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one.
     41ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen.
     42ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight.
     43ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine.
     44ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen.
     45ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight.
     46ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen.
     47ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight.
     48ndefinition two_hundred ≝ one_hundred + one_hundred.
     49ndefinition two_hundred_and_two ≝ two_hundred + two.
     50ndefinition two_hundred_and_three ≝ two_hundred_and_two + one.
     51ndefinition two_hundred_and_four ≝ two_hundred_and_three + one.
     52ndefinition two_hundred_and_five ≝ two_hundred_and_four + one.
     53ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three.
     54ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen.
     55ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
    3056ndefinition two_hundred_and_fifty_six ≝
    31   one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                        
     57  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                       
    3258   
    3359ndefinition nat_of_bool ≝
Note: See TracChangeset for help on using the changeset viewer.