Changeset 1607 for src/ASM/AssemblyProof.ma
- Timestamp:
- Dec 14, 2011, 1:50:23 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r1484 r1607 1314 1314 ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2. 1315 1315 1316 1317 notation < "❰ x ❱" with precedence 90 for @{'dp $x $y }.1318 interpretation "dp" 'dp x y = (dp x y).1319 1320 1316 lemma fetch_assembly_pseudo': 1321 1317 ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
Note: See TracChangeset
for help on using the changeset viewer.