Changeset 2682 for src/Clight/labelSimulation.ma
- Timestamp:
- Feb 19, 2013, 7:24:20 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/labelSimulation.ma
r2677 r2682 1021 1021 >shift_fst whd in match (seq_of_labeled_statement ?); 1022 1022 cases (step_with_labels_partial … RG (State f s k e m) (State (\fst (label_function u0 f)) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX) 1023 #n #H %{(S n)} @(after_n_m 1 (S n) … H) % /2/1023 #n #H %{(S n)} @(after_n_m 1 (S n) … H) // % /2/ 1024 1024 #trx #sx * /3/ 1025 1025 (* but for LScase it's just like the cases in step_with_labels_partial *)
Note: See TracChangeset
for help on using the changeset viewer.