Changeset 2316 for src/ASM/Status.ma


Ignore:
Timestamp:
Sep 3, 2012, 9:03:24 AM (8 years ago)
Author:
boender
Message:
  • committed temporary version: true version has to wait until I recuperate my hard disk
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r2272 r2316  
    10761076  ∀i.
    10771077    \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i →
    1078       instruction_has_label id i →
    1079         occurs_exactly_once ASMTag pseudo_instruction id instr_list.
     1078      (instruction_has_label id i →
     1079        occurs_exactly_once ASMTag pseudo_instruction id instr_list) ∧
     1080      (is_jump_to i id →
     1081        occurs_exactly_once ASMTag pseudo_instruction id instr_list).
    10801082
    10811083definition construct_datalabels: preamble → ? ≝
Note: See TracChangeset for help on using the changeset viewer.