Changeset 1962


Ignore:
Timestamp:
May 17, 2012, 12:25:41 AM (8 years ago)
Author:
sacerdot
Message:

More examples are now indexed.

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1938 r1962  
    127127  cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks
    128128  #classify_assm #classify_assm' @classify_assm' assumption
    129 qed-.
     129qed.
    130130
    131131lemma nat_of_bitvector_lt_bound:
  • src/ASM/Interpret.ma

    r1951 r1962  
    972972  [1,2,3,4,5,6,7,8:
    973973    normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
    974     try //
     974    try // (*CSC: Veeery slow*)
    975975    -s destruct(INSTR_PC) <instr_refl whd
    976976    try (#absurd normalize in absurd; try destruct(absurd) try %) %
  • src/ASM/StatusProofs.ma

    r1959 r1962  
    8181qed.
    8282
    83 example get_arg_8_set_program_counter:
     83lemma get_arg_8_set_program_counter:
    8484 ∀n.∀l:Vector addressing_mode_tag (S n).
    8585  ∀T,cm,s,pc,b.∀arg:l.
     
    184184qed. *)
    185185
    186 example set_arg_8_set_program_counter:
     186lemma set_arg_8_set_program_counter:
    187187  ∀n:nat.
    188188  ∀l:Vector addressing_mode_tag (S n).
Note: See TracChangeset for help on using the changeset viewer.