Skip to content
Snippets Groups Projects
Commit 1d1fe891 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

fix comment

parent d907c61a
No related branches found
No related tags found
No related merge requests found
Pipeline #117639 passed
Hide whitespace changes
Inline Side-by-side
analysis/definitions/finish_time.v
+ 1
− 1
View file @ 1d1fe891
...@@ -45,7 +45,7 @@ Section JobFinishTime. ...@@ -45,7 +45,7 @@ Section JobFinishTime.
Definition finish_time : instant := ex_minn job_finishes. Definition finish_time : instant := ex_minn job_finishes.
(** In the following, we demonstrate the reuse of [ex_minn] properties by (** In the following, we demonstrate the reuse of [ex_minn] properties by
establishing two natural properties of a job's finish time. *) establishing three natural properties of a job's finish time. *)
(** First, a job is indeed complete at its finish time. *) (** First, a job is indeed complete at its finish time. *)
Corollary finished_at_finish_time : completed_by sched j finish_time. Corollary finished_at_finish_time : completed_by sched j finish_time.
......
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