Ignore:
Timestamp:
Mar 21, 2011, 6:27:22 PM (9 years ago)
Author:
campbell
Message:

Refine small-step executable semantics abstraction a little.
Some progress on using the new definition in CexecEquiv?, but only partial
because of over-eager normalisation by the destruct tactic.
Whole program semantics for RTLabs using it.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r695 r702  
    1818(* *********************************************************************)
    1919
    20 include "Values.ma".
     20include "common/Values.ma".
    2121
    2222inductive constant : Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.