|
|
|
@1666
|
9 years |
sacerdot |
PreStatus? datatype change: the code_memory field is not a left …
|
|
|
|
@1600
|
9 years |
sacerdot |
utilities and ASM ported to the new standard library
|
|
|
|
@1599
|
9 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
|
@1588
|
9 years |
sacerdot |
All goals generated by Russell for execute_1* are now closed, mostly …
|
|
|
|
@1581
|
9 years |
mulligan |
Dangling de Bruijn pointer when trying to propagate russell to set_arg_1
|
|
|
|
@1541
|
9 years |
mulligan |
interpret.ma now compiles
|
|
|
|
@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
|
|
|
|
@1521
|
9 years |
sacerdot |
Syntax change in Matita: change what where => change where what.
|
|
|
|
@1518
|
9 years |
campbell |
Update to new syntax.
|
|
|
|
@1516
|
9 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
|
@1515
|
9 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
|
@1459
|
9 years |
boender |
- moved stronger occurs_exactly_once lemma to its proper place in …
|
|
|
|
@1393
|
9 years |
boender |
- added invariant for policy trie to assembly
- change (syntax only) …
|
|
|
|
@993
|
10 years |
sacerdot |
More Russell everywhere; getting closer to the goal.
|
|
|
|
@990
|
10 years |
sacerdot |
Do no longer use the daemon automatically :-)
|
|
|
|
@985
|
10 years |
sacerdot |
1) Major refactoring: proofs moved where they should be.
2) New …
|
|
|
|
@949
|
10 years |
mulligan |
resolved conflict, work from today
|
|
|
|
@935
|
10 years |
mulligan |
changes to status and assembly proof
|
|
|
|
@911
|
10 years |
sacerdot |
Type of set_code_memory generalized.
|
|
|
|
@843
|
10 years |
sacerdot |
Function moved from Interpret to Status.
|
|
|
|
@827
|
10 years |
sacerdot |
The preamble is now part of the PseudoStatus?.
|
|
|
|
@821
|
10 years |
mulligan |
changes to introduce pseudostatus
|
|
|
|
@757
|
10 years |
mulligan |
Lots more fixing to get both front and backends using same conventions …
|
|
|
|
@705
|
10 years |
sacerdot |
Ported to new library (notation).
|
|
|
|
@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/new-matita-development/Status.ma:
|
|
|
|
@688
|
10 years |
mulligan |
Fixed local conflicts. Restructured svn repository.
|
