Ignore:
Timestamp:
Dec 5, 2011, 5:16:55 PM (8 years ago)
Author:
mulligan
Message:

changes from today, including removing indexing of problematic function in utilities/binary/positive.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/binary/positive.ma

    r1528 r1587  
    852852
    853853theorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n.
    854 #n elim n; //; qed.
     854#n elim n; //; qed-.
    855855
    856856theorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)-m.
Note: See TracChangeset for help on using the changeset viewer.