Changeset 2651
- Timestamp:
- Feb 8, 2013, 11:13:07 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2516 r2651 594 594 lemma label_does_not_occur: 595 595 ∀i:ℕ.∀p:list labelled_instruction.∀l:Identifier. 596 is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur ?? l p = false.596 is_label (nth i ? p 〈None ?, Comment EmptyString〉) l → does_not_occur ?? l p = false. 597 597 #i #p #l generalize in match i; elim p 598 598 [ #i >nth_nil #H cases H
Note: See TracChangeset
for help on using the changeset viewer.