Changeset 949 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Jun 13, 2011, 6:42:14 PM (8 years ago)
Author:
mulligan
Message:

resolved conflict, work from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r744 r949  
    8888  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
    8989  @le_S @le_S @le_n (* ugly: fix using tacticals *)
     90qed.
     91
     92(* dpm: needed for assembly proof *)
     93definition sub_7_with_carry ≝
     94  λb, c: BitVector 7.
     95  λcarry: bool.
     96  sub_n_with_carry 7 b c carry ?.
     97  @le_S @le_S @le_n
    9098qed.
    9199
Note: See TracChangeset for help on using the changeset viewer.