

@1909

9 years 
mulligan 
Ported new statements to remainder of Interpret.ma file.



@1710

9 years 
mulligan 
changes from friday afternoon



@1709

9 years 
mulligan 
Changes to the execution of the MOVC instruction



@1666

9 years 
sacerdot 
PreStatus? datatype change: the code_memory field is not a left …



@1606

9 years 
sacerdot 
Porting to last library of Matita.



@1600

9 years 
sacerdot 
utilities and ASM ported to the new standard library



@1588

9 years 
sacerdot 
All goals generated by Russell for execute_1* are now closed, mostly …



@1587

9 years 
mulligan 
changes from today, including removing indexing of problematic …



@1582

9 years 
mulligan 
more added to the proof of execute_1_preinstruction  ~260 cases now …



@1581

9 years 
mulligan 
Dangling de Bruijn pointer when trying to propagate russell to set_arg_1



@1577

9 years 
mulligan 
A lot more cases added to the proof at the bottom of …



@1575

9 years 
mulligan 
Changes to specifications on execute functions



@1573

9 years 
mulligan 
more complicated than it appears :(



@1547

9 years 
sacerdot 
Invariant on cost of one execution step strengthened.



@1541

9 years 
mulligan 
interpret.ma now compiles



@1540

9 years 
mulligan 
changes to proof in interrupt.ma



@1538

9 years 
mulligan 
changes to execute_1_0 proof



@1534

9 years 
mulligan 
committing my changes to interpret to prevent any further conflicts



@1533

9 years 
sacerdot 
Proof of execute_1 with Russell completed (up to some daemon used before).



@1527

9 years 
sacerdot 
More on Russell.



@1526

9 years 
sacerdot 
Using Russell to prove some properties.



@1522

9 years 
mulligan 
changes to preamble and lin to asm pass, resolved conflict in interpret



@1519

9 years 
campbell 
More syntax updates.



@1515

9 years 
campbell 
Add type of maps on positive binary numbers, and use them for …



@1514

9 years 
mulligan 
changes from today. matita keeps dieing



@1511

9 years 
mulligan 
proofs, added, changes to execute_1_0 function therefore required to …



@1494

9 years 
mulligan 
changes to get everything compiling again



@1037

10 years 
sacerdot 
Main theorem: comments are working again.



@985

10 years 
sacerdot 
1) Major refactoring: proofs moved where they should be.
2) New …



@936

10 years 
sacerdot 
Ticks are now handled correctly everywhere and the main proof takes …



@928

10 years 
sacerdot 
Technical splitting.



@910

10 years 
mulligan 
removed bug in execute_1_pseudoinstruction



@865

10 years 
sacerdot 
Renaming.



@856

10 years 
sacerdot 
1. if_then_else is now a notation for match with (to allow Russell to …



@843

10 years 
sacerdot 
Function moved from Interpret to Status.



@827

10 years 
sacerdot 
The preamble is now part of the PseudoStatus?.



@825

10 years 
mulligan 
lots of refactoring, finally got something to prove



@822

10 years 
mulligan 
removed all axioms



@821

10 years 
mulligan 
changes to introduce pseudostatus



@820

10 years 
mulligan 
changes to get the semantics of pseudoassembly working



@757

10 years 
mulligan 
Lots more fixing to get both front and backends using same conventions …



@712

10 years 
mulligan 
Changes to get things to typecheck.



@698

10 years 
mulligan 
Commit with changes to files to get our files to typecheck.



@690

10 years 
mulligan 
Moved new matita files into correct place.


copied from src/ASM/newmatitadevelopment/Interpret.ma:



@688

10 years 
mulligan 
Fixed local conflicts. Restructured svn repository.
