Changeset 547


Ignore:
Timestamp:
Feb 16, 2011, 6:45:31 PM (6 years ago)
Author:
campbell
Message:

Add missing file.

Location:
Deliverables/D3.1/C-semantics
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Integers.ma

    r535 r547  
    9797definition intrange: ∀i:int. 0 ≤ (intval i) ∧ (intval i) < modulus.
    9898#i % whd in ⊢ (?%%)
    99 [ @Z_unsigned_min
    100 | @Z_unsigned_max
     99[ @bv_Z_unsigned_min
     100| @bv_Z_unsigned_max
    101101] qed.
    102102
Note: See TracChangeset for help on using the changeset viewer.