source: src @ 1489

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