

@1577

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



@1575

10 years 
mulligan 
Changes to specifications on execute functions



@1573

10 years 
mulligan 
more complicated than it appears :(



@1547

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



@1541

10 years 
mulligan 
interpret.ma now compiles



@1540

10 years 
mulligan 
changes to proof in interrupt.ma



@1538

10 years 
mulligan 
changes to execute_1_0 proof



@1534

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



@1533

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



@1527

10 years 
sacerdot 
More on Russell.



@1526

10 years 
sacerdot 
Using Russell to prove some properties.



@1522

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



@1519

10 years 
campbell 
More syntax updates.



@1515

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



@1514

10 years 
mulligan 
changes from today. matita keeps dieing



@1511

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



@1494

10 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

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



@712

11 years 
mulligan 
Changes to get things to typecheck.



@698

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



@690

11 years 
mulligan 
Moved new matita files into correct place.


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



@688

11 years 
mulligan 
Fixed local conflicts. Restructured svn repository.
