Changeset 1225


Ignore:
Timestamp:
Sep 16, 2011, 6:48:50 PM (8 years ago)
Author:
campbell
Message:

Missing ; in proof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1224 r1225  
    490490 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
    491491   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct >e0 //
    492    >e0 in e1 normalize #H @H ]
     492   >e0 in e1; normalize #H @H ]
    493493qed.
    494494
Note: See TracChangeset for help on using the changeset viewer.