 Timestamp:
 May 16, 2012, 4:47:56 PM (8 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r1952 r1958 26 26 whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta 27 27 lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc 28 inversion pi 29 [2,3: 30 #comment_or_cost #instr_refl #next_internal_pseudo_refl 31 %{0} @split_eq_status whd in match execute_1_pseudo_instruction; 32 whd in match execute_1_pseudo_instruction0; normalize nodelta 33 whd in match ticks_of0; normalize nodelta // 34 [1: 35 destruct /demod/ 36 2: 37 3: 38 4: 39 5: 40 6: 41 ] 42 28 43 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?) 29 44 [>EQ2 %] 
src/ASM/StatusProofs.ma
r1710 r1958 282 282 qed. 283 283 284 lemma set_clock_set_program_counter: 285 ∀T,cm,s,x,y. 286 set_clock T cm (set_program_counter … s x) y = 287 set_program_counter … (set_clock … s y) x. 288 // 289 qed. 290 284 291 lemma set_low_internal_ram_set_high_internal_ram: 285 292 ∀T,cm,s,x,y. … … 354 361 qed. 355 362 363 (* XXX: this was compiling before! *) 356 364 lemma program_counter_set_arg_1: 357 365 ∀m, cm, s, addr, v.
Note: See TracChangeset
for help on using the changeset viewer.