Changeset 1587 for src/utilities/binary

Timestamp:

Dec 5, 2011, 5:16:55 PM (10 years ago)

Author:

mulligan

Message:

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

File:

• src/utilities/binary/positive.ma (modified) (1 diff)

src/utilities/binary/positive.ma

@@ -852 +852 @@
 
 theorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n.
-#n elim n; //; qed.
+#n elim n; //; qed-.
 
 theorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)-m.