|
|
|
@2230
|
9 years |
sacerdot |
Glue proof maximally simplified or sort of.
|
|
|
|
@2229
|
9 years |
sacerdot |
More cleaning up, ready for more aggressive factorization.
|
|
|
|
@2228
|
9 years |
sacerdot |
Further proof reduction.
|
|
|
|
@2225
|
9 years |
sacerdot |
Minor and major improvements everywhere, shortened proofs.
|
|
|
|
@2211
|
9 years |
boender |
- finished proof of sigma specification
- added some stuff to Util, as …
|
|
|
|
@2153
|
9 years |
boender |
- updated the proof some more
|
|
|
|
@2152
|
9 years |
boender |
- this should compile
|
|
|
|
@2141
|
9 years |
boender |
- committed working version
|
|
|
|
@2101
|
9 years |
boender |
- renamed medium to absolute jump
- revised proofs of policy, some …
|
|
|
|
@2078
|
9 years |
sacerdot |
sigma_policy_specification has been
1) strengthened
2) made nicer to …
|
|
|
|
@2059
|
9 years |
boender |
- updated Policy to work better
|
|
|
|
@2055
|
9 years |
sacerdot |
Warning: this commit adds an hypothesis that breaks all of assembly stuff.
|
|
|
|
@2034
|
9 years |
boender |
- split Policy into three separate files for ease (and indeed …
|
|
|
|
@2032
|
9 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
|
@2018
|
9 years |
mulligan |
CJNE case a complete mess.
|
|
|
|
@2008
|
9 years |
boender |
- substantial closing of holes in proof
|
|
|
|
@1973
|
9 years |
boender |
- removed superfluous match
- displaced 'cases daemon'
|
|
|
|
@1965
|
9 years |
boender |
- further completed proof, changed jump_expansion' to reflect new type …
|
|
|
|
@1956
|
9 years |
boender |
- finished proof of lemma (where auto does strange things again)
|
|
|
|
@1950
|
9 years |
boender |
- advances in policy
|
|
|
|
@1942
|
9 years |
mulligan |
Work on showing the equivalence of two methods of looking up from the maps.
|
|
|
|
@1940
|
9 years |
boender |
- committed new version of final invariant
|
|
|
|
@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 …
|
|
|
|
@1933
|
9 years |
boender |
- slight revamp
|
|
|
|
@1932
|
9 years |
boender |
- added some more dependent types (we love 'em)
|
|
|
|
@1931
|
9 years |
boender |
- added latest bvt alias
- temporary "cases daemon" commit of new …
|
|
|
|
@1886
|
9 years |
boender |
- improvements for disambiguation and quick(er) typing
|
|
|
|
@1879
|
9 years |
boender |
- Policy compiles until the end, still some (fairly trivial) cases …
|
|
|
|
@1810
|
9 years |
boender |
- new version of policy that compiles up to the final glue
|
|
|
|
@1809
|
9 years |
boender |
- committed partially compiling version of policy (up until …
|
|
|
|
@1615
|
10 years |
sacerdot |
Policy now depends on Assembly and not the other way around.
|
|
|
|
@1614
|
10 years |
boender |
- split policy from assembly
|
