Changeset 1516 for src/common/GenMem.ma


Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/GenMem.ma

    r1395 r1516  
    5353  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
    5454  update_block … x v f x = v.
    55 #A * * #ix #v #f whd in ⊢ (??%?)
     55#A * * #ix #v #f whd in ⊢ (??%?);
    5656>eq_block_b_b //
    5757qed.
Note: See TracChangeset for help on using the changeset viewer.