Changeset 1880 for src/RTLabs/semantics.ma
- Timestamp:
- Apr 6, 2012, 4:57:22 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/semantics.ma
r1878 r1880 326 326 ] qed. 327 327 328 329 lemma initial_state_is_not_final : ∀p,s. 330 make_initial_state p = OK ? s → 331 RTLabs_is_final s = None ?. 332 #p #s whd in ⊢ (??%? → ?); 333 @bind_ok #m #Em 334 @bind_ok #b #Eb 335 @bind_ok #f #Ef 336 #E destruct 337 @refl 338 qed.
Note: See TracChangeset
for help on using the changeset viewer.