source: src/ASM/AssemblyProof.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @871   9 years sacerdot
(edit) @870   9 years mulligan more changes
(edit) @869   9 years sacerdot More progress.
(edit) @868   9 years mulligan more changes
(edit) @867   9 years mulligan changes to assembly proof
(edit) @866   9 years sacerdot Significant improvement in the proof.
(edit) @865   9 years sacerdot Renaming.
(edit) @864   9 years mulligan resolved conflict
(edit) @863   9 years sacerdot Yet another fix to the statement.
(edit) @862   9 years sacerdot
(edit) @861   9 years sacerdot Statement of the lemma fixed (again!) Some preliminary work on …
(edit) @860   9 years sacerdot Progress in the proof.
(edit) @859   9 years mulligan more added
(edit) @856   9 years sacerdot 1. if_then_else is now a notation for match with (to allow Russell to …
(edit) @855   9 years mulligan changes from today
(edit) @854   9 years mulligan commit to avoid conflicts
(edit) @853   9 years sacerdot
(edit) @852   9 years mulligan foldl_strong outer definition
(edit) @851   9 years mulligan strong foldl added
(edit) @850   9 years sacerdot More informative foldl: foldll.
(edit) @849   9 years sacerdot
(edit) @848   9 years sacerdot
(edit) @847   9 years sacerdot Several bugs fixed in Matita.
(edit) @846   9 years mulligan changes
(edit) @845   9 years sacerdot Nightmare…
(edit) @841   9 years sacerdot Minor changes.
(edit) @840   9 years sacerdot sigma defined
(edit) @839   9 years sacerdot More experiments.
(edit) @838   9 years sacerdot Restored.
(edit) @835   9 years sacerdot Old experiments removed.
(edit) @834   9 years sacerdot Russell at work.
(edit) @833   9 years sacerdot Bug fixed to make the file compile. But the type of the assembly …
(edit) @832   9 years mulligan work from today
(edit) @831   9 years sacerdot Progress in proofs.
(edit) @829   9 years sacerdot
(edit) @828   9 years sacerdot Proof statement.
(edit) @827   9 years sacerdot The preamble is now part of the PseudoStatus?.
(edit) @826   9 years mulligan start of proof
(edit) @825   9 years mulligan lots of refactoring, finally got something to prove
(add) @823   9 years mulligan added new file for proof of correctness of pseudo-assembly translation
Note: See TracRevisionLog for help on using the revision log.