

@2316

8 years 
boender 
 committed temporary version: true version has to wait until I …



@2272

8 years 
mulligan 
Changed proof strategy for main lemma after noticed that the current …



@2270

8 years 
mulligan 
Bug spotted and fixed in write_at_stack_pointer



@2264

8 years 
sacerdot 
1) Major change: we now always use the efficient way of resolving …



@2247

8 years 
mulligan 
Work on the MOV instruction from today and bug fixes in set_arg_1.



@2172

8 years 
mulligan 
Moved new versions of get_ / set_arg_* into Status.ma. Commented out …



@2160

8 years 
mulligan 
Added a new scratch file Test.ma for working on lemmas that are needed …



@2139

8 years 
mulligan 
Changes to get the main lemma compiling again. Changes pushed into …



@2123

8 years 
boender 
 moved is_well_labeled_p to Status and instruction_is_label to ASM
…



@2119

8 years 
sacerdot 
load_code_memory moved to Fetch.ma and proved correct w.r.t. next …



@2111

8 years 
sacerdot 
Cleanup: lemmas/theorems/axioms moved to the right places.



@2055

8 years 
sacerdot 
Warning: this commit adds an hypothesis that breaks all of assembly stuff.



@2032

8 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@1946

8 years 
sacerdot 
\snd half_add => add everywhere



@1882

8 years 
tranquil 
big update, alas incomplete:
joint changed a bit, and all BE languages …



@1666

8 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

9 years 
sacerdot 
More Russell everywhere; getting closer to the goal.



@990

9 years 
sacerdot 
Do no longer use the daemon automatically :)



@985

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



@949

9 years 
mulligan 
resolved conflict, work from today



@935

9 years 
mulligan 
changes to status and assembly proof



@911

9 years 
sacerdot 
Type of set_code_memory generalized.



@843

9 years 
sacerdot 
Function moved from Interpret to Status.



@827

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



@821

9 years 
mulligan 
changes to introduce pseudostatus



@757

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



@705

9 years 
sacerdot 
Ported to new library (notation).



@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/Status.ma:



@688

9 years 
mulligan 
Fixed local conflicts. Restructured svn repository.
