Commit 21162035 authored by Marco Maida's avatar Marco Maida 🌱
Browse files

More polish

parent 658fdefc
Pipeline #24110 passed with stages
in 3 minutes and 40 seconds
......@@ -241,7 +241,7 @@ Section AuxiliaryLemmasWorkConservingTransformation.
(** ...let [t_swap] be a time instant found by the search procedure. *)
Variable t_swap: instant.
Hypothesis search_result_found : search_result = Some t_swap.
Hypothesis search_result_found: search_result = Some t_swap.
(** We show that, since the search only yields relevant processor states, a job is found. *)
Lemma make_wc_at_case_result_found:
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment