

@1528

8 years 
campbell 
Update most of Assembly.ma with new syntax and identifier maps.
Change …



@1493

8 years 
mulligan 
finished well labeled check, up to injectivity of the label map



@1482

8 years 
sacerdot 
1. very long standing conflict committed (but don't ask me what the …



@1479

8 years 
boender 
 added insert_lookup_opt
 assembly compiles now



@1459

8 years 
boender 
 moved stronger occurs_exactly_once lemma to its proper place in …



@1417

8 years 
boender 
 proved that jumps always increase  this should make termination easy



@1404

8 years 
boender 
 reworked + added
 added an axiom to arithmetic, but should be provable



@1393

8 years 
boender 
 added invariant for policy trie to assembly
 change (syntax only) …



@1363

8 years 
boender 
 done stuff with create_label_trie



@1309

8 years 
boender 
 refounded JEP



@1103

9 years 
boender 
 reverted to old policy



@1054

9 years 
boender 
 proven policy safe



@1040

9 years 
sacerdot 
Bug fixed in assembly.



@1014

9 years 
sacerdot 
The main theorem is completely broken (again).



@998

9 years 
sacerdot 
Half repaired, half broken. Most functions no longer return option …



@993

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



@989

9 years 
sacerdot 
Type of build_maps strengthened.



@987

9 years 
sacerdot 
Real parameterization over the policy.



@985

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



@982

9 years 
boender 
 this should work (see previous commit)



@938

9 years 
sacerdot 
…



@922

9 years 
mulligan 
changes to get assemblyproof to compile



@920

9 years 
boender 
 corrected mov instruction



@914

9 years 
boender 
 complete.



@913

9 years 
boender 
 temporary commit s.t. Assembly compiles



@907

9 years 
boender 
 added quadruples to Util
 start of implementation of new jump …



@846

9 years 
mulligan 
changes



@844

9 years 
sacerdot 
Useless code removed.



@842

9 years 
sacerdot 
Bug fixed.



@840

9 years 
sacerdot 
sigma defined



@837

9 years 
mulligan 
changes complete



@836

9 years 
mulligan 
changes to assembly functions



@833

9 years 
sacerdot 
Bug fixed to make the file compile.
But the type of the assembly …



@832

9 years 
mulligan 
work from today



@825

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



@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 …



@719

9 years 
mulligan 
Added missing assembly file ported to matita.
