source: src @ 1489

Name Size Rev Age Author Last Change
../
RTLabs 1408   10 years sacerdot 1. Added joint/BEGlobalenvs that is a modification of …
RTL 1481   10 years sacerdot Proof fixed. The new standard library does not index any longer the …
LTL 1451   10 years sacerdot 1. All axioms in LIN/semantics.ma closed 2. succ_pc and …
LIN 1451   10 years sacerdot 1. All axioms in LIN/semantics.ma closed 2. succ_pc and …
common 1480   10 years sacerdot Proof changed (to use new automation). BUG FOUND: automation fails if …
utilities 1463   10 years mulligan added erasure for lin
joint 1472   10 years mulligan moved proof utils to erasure.ma
ERTL 1463   10 years mulligan added erasure for lin
ASM 1487   10 years mulligan committing some code for well labelling
Cminor 1464   10 years campbell Use unification hints to simplify the graph monotonicity proofs.
Clight 1489   10 years campbell Fix up a couple of lemmas affected by the change to add_with_carries.
TODO 606 bytes 1457   10 years sacerdot Bug fixed: when calling an internal function, the pc block is now set …
root 26 bytes 703   10 years sacerdot lib is now the default standard library (after commit 11216 in …
CHANGES 3.4 KB 1388   10 years sacerdot fetch_result implemented for ERTL. This required a different …
acc-matita-printers.patch 7.3 KB 1158   10 years campbell Record patch needed to use matita pretty printers with acc.
Note: See TracBrowser for help on using the repository browser.