|
|
|
@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
|
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/new-matita-development/Interpret.ma:
|
|
|
|
@688
|
9 years |
mulligan |
Fixed local conflicts. Restructured svn repository.
|
