Changeset 1618 for src/Clight/test
- Timestamp:
- Dec 14, 2011, 6:17:53 PM (9 years ago)
- Location:
- src/Clight/test
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/test/search.c.ma
r1599 r1618 215 215 @refl 216 216 qed. 217 217 (* 218 218 example csc: True. 219 219 letin yyy ≝ ( … … 228 228 letin zzz ≝ (do p ← yyy ; rtlabs_to_rtl p) 229 229 @⊥ normalize in xxx; 230 *) -
src/Clight/test/sum.test.ma
r1599 r1618 33 33 @refl 34 34 qed. 35 35 (* 36 36 include "RTLabs/RTLabsToRTL.ma". 37 37 include alias "basics/lists/list.ma". … … 60 60 [2: check (joint_if_code (prog_var_names … p) ? f) |3: cases daemon ] 61 61 normalize in xxx 62 62 *)
Note: See TracChangeset
for help on using the changeset viewer.