Ignore:
Timestamp:
Dec 11, 2010, 4:16:00 PM (9 years ago)
Author:
campbell
Message:

Minor changes for the new version of matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/binary/Z.ma

    r15 r400  
    553553   ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
    554554   ##|#p;nrewrite < (Zsucc_Zplus_pos_O …); //]
    555 ##|ncases y;/2/; #p; nrewrite > (sym_Zplus (Zpred OZ));
    556    nrewrite < (Zpred_Zplus_neg_O …); //;
     555##|ncases y;/2/; #p; nrewrite > (sym_Zplus ? (Zpred OZ));
     556   nrewrite < Zpred_Zplus_neg_O; //;
    557557##|ncases y
    558558   ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
Note: See TracChangeset for help on using the changeset viewer.