Ignore:
Timestamp:
Dec 14, 2011, 1:50:23 PM (8 years ago)
Author:
sacerdot
Message:

Porting to new library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1484 r1607  
    13141314  ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
    13151315               
    1316 
    1317 notation < "❰ x ❱" with precedence 90 for @{'dp $x $y }.
    1318 interpretation "dp" 'dp x y = (dp x y).
    1319 
    13201316lemma fetch_assembly_pseudo':
    13211317 ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
Note: See TracChangeset for help on using the changeset viewer.