

@1606

8 years 
sacerdot 
Porting to last library of Matita.



@1600

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



@1588

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



@1587

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



@1582

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



@1581

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



@1577

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



@1575

8 years 
mulligan 
Changes to specifications on execute functions



@1573

8 years 
mulligan 
more complicated than it appears :(



@1547

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



@1541

8 years 
mulligan 
interpret.ma now compiles



@1540

8 years 
mulligan 
changes to proof in interrupt.ma



@1538

8 years 
mulligan 
changes to execute_1_0 proof



@1534

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



@1533

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



@1527

8 years 
sacerdot 
More on Russell.



@1526

8 years 
sacerdot 
Using Russell to prove some properties.



@1522

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



@1519

8 years 
campbell 
More syntax updates.



@1515

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



@1514

8 years 
mulligan 
changes from today. matita keeps dieing



@1511

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



@1494

8 years 
mulligan 
changes to get everything compiling again



@1037

9 years 
sacerdot 
Main theorem: comments are working again.



@985

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



@936

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



@928

9 years 
sacerdot 
Technical splitting.



@910

9 years 
mulligan 
removed bug in execute_1_pseudoinstruction



@865

9 years 
sacerdot 
Renaming.



@856

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



@843

9 years 
sacerdot 
Function moved from Interpret to Status.



@827

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



@825

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



@822

9 years 
mulligan 
removed all axioms



@821

9 years 
mulligan 
changes to introduce pseudostatus



@820

9 years 
mulligan 
changes to get the semantics of pseudoassembly working



@757

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



@712

9 years 
mulligan 
Changes to get things to typecheck.



@698

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



@690

9 years 
mulligan 
Moved new matita files into correct place.


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



@688

9 years 
mulligan 
Fixed local conflicts. Restructured svn repository.
