source:
src/ERTLptr
@
2868
| Name | Size | Rev | Age | Author | Last Change |
|---|---|---|---|---|---|
| ../ | |||||
| ERTLptr.ma | 2.1 KB | 2783 | 7 years | modified joint_closed_internal_function definition (added condition on … | |
| ERTLptr_printer.ma | 1.3 KB | 2868 | 7 years | Pretty printing of ERTL and ERTLptr code. | |
| ERTLptr_semantics.ma | 2.6 KB | 2796 | 7 years | * added global notation for existence in Type[1] (\exists[1] x.P) * in … | |
| ERTLptrToLTL.ma | 16.3 KB | 2844 | 7 years | Stupid bug fixed | |
| ERTLptrToLTLProof.ma | 15.4 KB | 2863 | 7 years | Added new invariant to good_if Generalized version of cond case for … | |
| Interference.ma | 995 bytes | 2845 | 7 years | ERTLptr to LTL correctness proof started | |
| liveness.ma | 9.6 KB | 2700 | 7 years | 1. exponential function dropped in favour of standard library 2. … | |
| uses.ma | 3.0 KB | 2741 | 7 years | File used only by untrusted code. Implemented in Matita to exploit … | |
Note: See TracBrowser
for help on using the repository browser.
