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