Changeset 2459 for src/common


Ignore:
Timestamp:
Nov 13, 2012, 6:30:55 PM (7 years ago)
Author:
campbell
Message:

Syntax update

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r2444 r2459  
    207207
    208208lemma await_value_bind_inv : ∀avs,T,f,g,P.
    209   await_value avs (f »= g) P →
     209  await_value avs (m_bind … f g) P →
    210210  ∃x:T. (f = return x) ∧ await_value avs (g x) P.
    211211#avs #T *
Note: See TracChangeset for help on using the changeset viewer.