Changeset 723 for src/CHANGES


Ignore:
Timestamp:
Mar 30, 2011, 12:34:25 PM (9 years ago)
Author:
mulligan
Message:

Added dependent type internalising the invariant that LIN function bodies are non-empty and do not start with a label.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/CHANGES

    r721 r723  
    1010
    1111  Formalised missing Assembly.ma file.
     12
     1330/03/2011:
     14  Split translate_statements into two functions.
     15
     16  Added a dependent type for the invariant that a LIN function body does not
     17  start with a label, and is not empty.
Note: See TracChangeset for help on using the changeset viewer.