source:
src/ERTL
@
2970
| Name | Size | Rev | Age | Author | Last Change |
|---|---|---|---|---|---|
| ../ | |||||
| ERTL.ma | 5.2 KB | 2952 | 7 years | * corrected all back-end premains to not pass any arguments to the … | |
| ERTL_printer.ma | 1.2 KB | 2868 | 7 years | Pretty printing of ERTL and ERTLptr code. | |
| ERTL_semantics.ma | 6.0 KB | 2946 | 7 years | main novelties: * there is an in-built stack_usage nat in joint … | |
| ERTLToERTLptr.ma | 4.9 KB | 2843 | 7 years | 1) Fixed a litte bug in Joint.ma 2) ERTL to ERTLptr correctness proof … | |
| ERTLToERTLptrAxiom.ma | 1.7 KB | 2946 | 7 years | main novelties: * there is an in-built stack_usage nat in joint … | |
| ERTLtoERTLptrOK.ma | 68.7 KB | 2943 | 7 years | Mauro, I have put a daemon in place of the proof obligation that used … | |
| ERTLtoERTLptrUtils.ma | 77.1 KB | 2946 | 7 years | main novelties: * there is an in-built stack_usage nat in joint … | |
Note: See TracBrowser
for help on using the repository browser.
