Ignore:
Timestamp:
May 24, 2012, 5:10:05 PM (7 years ago)
Author:
campbell
Message:

Make front-end memory model only depend on the general definitions by
moving a few definitions from the back-end one. Give the front-end
model a more descriptive name.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Animation.ma

    r1881 r1993  
    9595fw_ok : ∀r,S,t,s. finishes_with r S (OK ? (finished S t r s)).
    9696
    97 include "common/Mem.ma".
     97include "common/GenMem.ma".
    9898
    9999(* Hide the representation of memory to make displaying the results easier. *)
Note: See TracChangeset for help on using the changeset viewer.