|
|
@2314
|
8 years |
campbell |
Move generic definitions from recent commit to appropriate places.
|
|
|
@2307
|
8 years |
campbell |
Half the proofs for sound cost labelling check.
|
|
|
@2286
|
8 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
@2211
|
9 years |
boender |
- finished proof of sigma specification
- added some stuff to Util, as …
|
|
|
@2149
|
9 years |
sacerdot |
Code shuffling to proper places.
|
|
|
@2125
|
9 years |
boender |
- some more displacement from Policy to Util
|
|
|
@2124
|
9 years |
sacerdot |
Much more shuffling around to proper places
|
|
|
@2123
|
9 years |
boender |
- moved is_well_labeled_p to Status and instruction_is_label to ASM
…
|
|
|
@2111
|
9 years |
sacerdot |
Cleanup: lemmas/theorems/axioms moved to the right places.
|
|
|
@2055
|
9 years |
sacerdot |
Warning: this commit adds an hypothesis that breaks all of assembly stuff.
|
|
|
@2037
|
9 years |
sacerdot |
flatten is now part of stdlib
|
|
|
@2032
|
9 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
@2005
|
9 years |
boender |
- minor changes to make things compile with a clean checkout
|
|
|
@1964
|
9 years |
tranquil |
introduced as_label_of_cost and adapted accordingly. Equality of cost …
|
|
|
@1937
|
9 years |
boender |
- filled in some of the gaps in the proof of Policy
- reverted …
|
|
|
@1934
|
9 years |
boender |
- various & sundry moves of lemmas to better places
- integrated …
|
|
|
@1928
|
9 years |
mulligan |
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
|
|
|
@1908
|
9 years |
fguidi |
notation fixup following last commit of matita
we shifted the levels …
|
|
|
@1882
|
9 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
@1811
|
9 years |
boender |
- corrected definition of geb
|
|
|
@1602
|
9 years |
mulligan |
giving up on fetch proofs for time being
|
|
|
@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.
|
|
|
@1598
|
9 years |
mulligan |
changes over the last couple of days
|
|
|
@1516
|
9 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
@1323
|
9 years |
campbell |
Reduce number of notations for destructive let on pairs to one.
|
|
|
@1279
|
9 years |
sacerdot |
Bug fixed in definition of ltb.
|
|
|
@1193
|
9 years |
mulligan |
work on colouring algorithm halted as it can be axiomatised. now …
|
|
|
@1161
|
9 years |
mulligan |
changes from today: merged ertl, ltl and lin into one datatype to …
|
|
|
@1159
|
9 years |
boender |
- added 'nth' theorems
- moved up \bot a bit
|
|
|
@1094
|
10 years |
mulligan |
some changes from today to do with liveness analyses
|
|
|
@1075
|
10 years |
mulligan |
nearly completed rtl -> ertl pass removing all option types with dep. types
|
|
|
@1071
|
10 years |
mulligan |
changes the specific form that the added proofs take to use None, not …
|
|
|
@1064
|
10 years |
mulligan |
changes from today, nearly complete rtlabs translation pass
|
|
|
@1063
|
10 years |
mulligan |
changes from today
|
|
|
@1062
|
10 years |
mulligan |
separated jmeq and coercions from foldstuff.ma in order to fix the …
|
|
|
@1061
|
10 years |
mulligan |
more work, bug found, ridiculous map3 function with dep. types added
|
|
|
@1060
|
10 years |
mulligan |
work from this morning and yesterday
|
|
|
@1059
|
10 years |
mulligan |
work from today, bit of a mess at the moment
|
|
|
@1057
|
10 years |
mulligan |
changes from today
|
|
|
@998
|
10 years |
sacerdot |
Half repaired, half broken. Most functions no longer return option …
|
|
|
@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 …
|
|
|
@907
|
10 years |
boender |
- added quadruples to Util
- start of implementation of new jump …
|
|
|
@900
|
10 years |
sacerdot |
New implementation of flatten was bugged: fixed.
|
|
|
@899
|
10 years |
mulligan |
changed defn. of flatten
|
|
|
@858
|
10 years |
sacerdot |
If then else notation improved.
|
|
|
@857
|
10 years |
sacerdot |
Notations.
|
|
|
@856
|
10 years |
sacerdot |
1. if_then_else is now a notation for match with (to allow Russell to …
|
|
|
@782
|
10 years |
mulligan |
More work on rtl-ertl pass from today, plus resolved conflict.
|
|
|
@777
|
10 years |
mulligan |
Lots of work on RTL to ERTL pass from today.
|
|
|
@764
|
10 years |
campbell |
Start Cminor to RTLabs phase.
Includes some syntax for matching …
|
|
|
@746
|
10 years |
mulligan |
Changes to bitvectortrieset: equality on sets. Added new file for …
|
|
|
@715
|
10 years |
mulligan |
Restored rev from Util as it appears that list reversal is not a part …
|
|
|
@712
|
10 years |
mulligan |
Changes to get things to typecheck.
|
|
|
@704
|
10 years |
sacerdot |
Minor speedup in one theorem (less automation).
|
|
|
@698
|
10 years |
mulligan |
Commit with changes to files to get our files to typecheck.
|
|
|
@697
|
10 years |
campbell |
Merge Clight branch of vectors and friends.
Start making stuff build.
|
|
|
@690
|
10 years |
mulligan |
Moved new matita files into correct place.
|
|
copied from src/ASM/new-matita-development/Util.ma:
|
|
|
@688
|
10 years |
mulligan |
Fixed local conflicts. Restructured svn repository.
|