Changeset 1607 for src/ASM/AssemblyProof.ma

Timestamp:

Dec 14, 2011, 1:50:23 PM (9 years ago)

Author:

sacerdot

Message:

Porting to new library.

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -1314 +1314 @@
   ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
                
-
-notation < "❰ x ❱" with precedence 90 for @{'dp $x $y }.
-interpretation "dp" 'dp x y = (dp x y). 
-
 lemma fetch_assembly_pseudo':
  ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.