

@470

9 years 
mulligan 
Finished moving development over to standard library.



@466

9 years 
mulligan 
Most of execute_1 checked. Need to fix negations, though, in rest in …



@465

9 years 
mulligan 
Moved over to standard library.



@439

9 years 
mulligan 
Changes to get everything to compile.



@374

9 years 
sacerdot 
1) notation for cast fixed
2) ambiguity reduced: Empty => VEmpty, Cons …



@372

9 years 
sacerdot 
No more axioms! All proofs completed.
(Interrupts, I/O and timers not …



@370

9 years 
mulligan 
Most of critical lemma done. Hole remaining that I can't coax matita …



@369

9 years 
mulligan 
Proof of missing lemma seems to be done, but won't Qed. My version of …



@368

9 years 
mulligan 
All 450 proof obligations closed.



@367

9 years 
mulligan 
Added decidable equality for addressing_mode_tags.



@364

9 years 
mulligan 
Added subvector_with function.



@363

9 years 
mulligan 
Resolved conflicts. Added new get_index' which hides the proof …



@362

9 years 
sacerdot 
Less ambiguous definitions.



@358

9 years 
mulligan 
Added \bot to all absd cases in execute_1 to get rid of as many open …



@357

9 years 
sacerdot 
 stupid bug fixed in BitVectorTrie?
 dependencies minimized, dead …



@351

9 years 
mulligan 
No more axioms but the paralogisms.



@347

9 years 
mulligan 
Work on main execution loop. All cases covered. Need to close open …



@343

9 years 
mulligan 
Fixed Status.ma so that it compiles.



@341

9 years 
sacerdot 
A simple version of assembly (no labels) implemented.



@338

9 years 
mulligan 
Most jumps finished. Only CJNE to do.



@337

9 years 
mulligan 
Changes to execute_1 file. Changes to get everything type checking.



@334

9 years 
mulligan 
More added.



@333

9 years 
mulligan 
Work on execute_1 function.



@331

9 years 
mulligan 
More changes to get everything to typecheck.



@329

9 years 
mulligan 
Commit to restore deleted file.



@328

9 years 
mulligan 
Got fold_right_i to type check. Moved eq_rect_Type0 into …
