source: src @ 1513

Name Size Rev Age Author Last Change
../
ASM 1511   10 years mulligan proofs, added, changes to execute_1_0 function therefore required to …
Clight 1513   10 years campbell Fix up Clight examples.
Cminor 1464   10 years campbell Use unification hints to simplify the graph monotonicity proofs.
common 1512   10 years campbell Shorten proof of goal that solves now.
ERTL 1463   10 years mulligan added erasure for lin
joint 1472   10 years mulligan moved proof utils to erasure.ma
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 …
utilities 1463   10 years mulligan added erasure for lin
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.