Changeset 1139 for src/Clight/CexecSound.ma
 Timestamp:
 Aug 30, 2011, 12:47:18 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecSound.ma
r1058 r1139 533 533 qed. 534 534 535 lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).535 lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? (fst ??) p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p). 536 536 #p cases p; #fns #main #vars 537 537 whd in ⊢ (???%);
Note: See TracChangeset
for help on using the changeset viewer.