

@2700

7 years 
sacerdot 
1. exponential function dropped in favour of standard library
2. …



@2688

7 years 
tranquil 
* in Arithmeticcs.ma: commented include that breaks script in latest …



@2684

7 years 
sacerdot 
…



@2673

7 years 
tranquil 
corrected some compilation errors (that might depend on some matita update)



@2672

7 years 
sacerdot 
One less axiom on bitvectors.



@2311

7 years 
garnier 
Some more cleaning of switchRemoval …



@2192

8 years 
sacerdot 
Shuffling around.



@2177

8 years 
campbell 
Tidy up multiplication.



@2154

8 years 
sacerdot 
Code shuffled around.



@2149

8 years 
sacerdot 
Code shuffling to proper places.



@2124

8 years 
sacerdot 
Much more shuffling around to proper places



@2111

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



@2108

8 years 
mulligan 
Various axioms closed and others moved around. Uncommented main lemma …



@2032

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



@2028

8 years 
boender 
 bugfix to Assembly (forgotten sigma)
 added …



@1963

8 years 
sacerdot 
More progress in restoring the original proof.



@1955

8 years 
mulligan 
Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some …



@1946

8 years 
sacerdot 
\snd half_add => add everywhere



@1934

8 years 
boender 
 various & sundry moves of lemmas to better places
 integrated …



@1928

8 years 
mulligan 
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …



@1870

8 years 
boender 
 changed sigma00 in Assembly to use foldl_strong + proved invariants …



@1646

8 years 
mulligan 
finished the block_costs computation, and propagated the changes …



@1599

8 years 
sacerdot 
Start of merging of stuff into the standard library of Matita.



@1485

8 years 
sacerdot 
Less nice definitiion of add_with_carries that avoids a quadratic …



@1426

8 years 
boender 
removed axiom



@1404

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



@1207

8 years 
campbell 
Second part of fixing temporaries in Clight to Cminor stage.



@961

9 years 
campbell 
Use precise bitvector sizes throughout the front end, rather than …



@949

9 years 
mulligan 
resolved conflict, work from today



@744

9 years 
campbell 
Evict Coqstyle integers from common/Integers.ma.
Make more bitvector …



@724

9 years 
campbell 
More tractable version of bitvector_of_nat / nat_of_bitvector.



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



@697

9 years 
campbell 
Merge Clight branch of vectors and friends.
Start making stuff build.



@690

9 years 
mulligan 
Moved new matita files into correct place.


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



@688

9 years 
mulligan 
Fixed local conflicts. Restructured svn repository.
