Ignore:
Timestamp:
Aug 2, 2012, 1:58:14 PM (7 years ago)
Author:
sacerdot
Message:
  1. duplicated code erased
  2. POP case finished up to lemmas on read_at_stack_pointer
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofs.ma

    r2272 r2285  
    6868lemma get_8051_sfr_set_program_counter:
    6969 ∀T,cm,s,pc. get_8051_sfr T cm (set_program_counter … s pc) = get_8051_sfr … s.
     70 //
     71qed.
     72
     73lemma get_8051_sfr_set_clock:
     74 ∀T,cm,s,pc. get_8051_sfr T cm (set_clock … s pc) = get_8051_sfr … s.
    7075 //
    7176qed.
Note: See TracChangeset for help on using the changeset viewer.