source: src/ASM/ASMCostsSplit.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2907   7 years sacerdot 1. a few bugs fixed 2. as_return implemented for ASM & OC
(edit) @2899   7 years sacerdot 1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system …
(edit) @2760   7 years sacerdot 1. Many files repaired. 2. 3 new daemons: 2 in Assembly.ma, 1 in …
(edit) @2754   7 years sacerdot 1. WARNING: I commented out one of James's function used in …
(edit) @2665   7 years sacerdot
(edit) @2657   7 years sacerdot Cost proof fully repaired. It was broken by the definitions used in …
(edit) @2516   7 years mckinna removed typedefs; restored older versions; moved typedefs to …
(edit) @2508   7 years mckinna more tweaks. compiler and correctness still build.
(edit) @2504   7 years mckinna More refactoring to support the tidied up compiler.ma
(edit) @2498   7 years mckinna Refactor: Typedefs object_code and costlabel_map lifted out from …
(edit) @2475   7 years campbell Get compiler.ma and correctness.ma checking again. Note that the …
(edit) @2001   8 years campbell Get the compiler to output more.
(edit) @1946   8 years sacerdot \snd half_add => add everywhere
(edit) @1929   8 years mulligan Simplified proof by removing most of the invariants on the statements …
(edit) @1928   8 years mulligan Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
(edit) @1921   8 years mulligan Horror proof mostly finished (compiles all way until end of CostsProof?.ma).
(edit) @1919   8 years mulligan Fixes to get everything compiling again
(edit) @1899   8 years mulligan Changes to statements of theorems
(edit) @1897   8 years mulligan Changes to proof, and pushed through those changes to rest of the file.
(edit) @1896   8 years mulligan Finished horror proof
(add) @1895   8 years mulligan Split the ASMCosts files while working on traverse_code_internal. A …
Note: See TracRevisionLog for help on using the revision log.