

@2178

8 years 
campbell 
Shift some notation into utilities.



@2101

8 years 
boender 
 renamed medium to absolute jump
 revised proofs of policy, some …



@2006

9 years 
boender 
 added alias for bitvector zero
 changed extralib bounded …



@1949

9 years 
tranquil 
* lemma trace rel to eq flatten trace
* some more properties of …



@1930

9 years 
campbell 
Tidy up labelling simulation stuff a bit.



@1882

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



@1599

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



@1593

9 years 
boender 
 cleaned up Assembly, moved some definitions elsewhere



@1523

9 years 
campbell 
Separate out positive and Z definitions from extralib.ma.
Minor 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 …



@1350

9 years 
sacerdot 
Porting to latest destruct tactic.
Note: the tactics has a few …



@1338

9 years 
sacerdot 
Automation is now stronger.



@1337

9 years 
sacerdot 
Automation is now stronger.



@1316

9 years 
campbell 
Merge in idlookupbranch to trunk.



@1260

9 years 
mulligan 
commit for csc



@1250

9 years 
sacerdot 
1. Sigma types projections moved to utilities/extralib.ma
2. Extended …



@891

10 years 
campbell 
Revise proofs affected by recent matita change.



@882

10 years 
campbell 
Fix up fragile proofs for current version of matita.



@711

10 years 
sacerdot 
…



@709

10 years 
sacerdot 
Notations should NOT be redefined. Just add a new interpretation.



@697

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



@695

10 years 
campbell 
Rearrange Clight files a bit  will try to make them work again soon…


copied from src/Clight/extralib.ma:



@694

10 years 
campbell 
Start moving Clight into common directory.
