introduce [rt_auto] and [rt_eauto] tactics
This commit renames scope [basic_facts] into [basic_rt_facts] to highlight the that lemmas collected in the scope are real-time (rt) theory lemmas. These new tactics are just shorthand for [(e)auto with basic_rt_facts].
Showing
- analysis/abstract/ideal_jlfp_rta.v 1 addition, 1 deletionanalysis/abstract/ideal_jlfp_rta.v
- analysis/facts/behavior/arrivals.v 72 additions, 7 deletionsanalysis/facts/behavior/arrivals.v
- analysis/facts/behavior/completion.v 2 additions, 2 deletionsanalysis/facts/behavior/completion.v
- analysis/facts/busy_interval/busy_interval.v 13 additions, 15 deletionsanalysis/facts/busy_interval/busy_interval.v
- analysis/facts/busy_interval/carry_in.v 3 additions, 4 deletionsanalysis/facts/busy_interval/carry_in.v
- analysis/facts/busy_interval/priority_inversion.v 9 additions, 9 deletionsanalysis/facts/busy_interval/priority_inversion.v
- analysis/facts/model/ideal_schedule.v 2 additions, 2 deletionsanalysis/facts/model/ideal_schedule.v
- analysis/facts/model/preemption.v 1 addition, 1 deletionanalysis/facts/model/preemption.v
- analysis/facts/model/rbf.v 1 addition, 1 deletionanalysis/facts/model/rbf.v
- analysis/facts/periodic/arrival_separation.v 4 additions, 4 deletionsanalysis/facts/periodic/arrival_separation.v
- analysis/facts/periodic/sporadic.v 2 additions, 2 deletionsanalysis/facts/periodic/sporadic.v
- analysis/facts/periodic/task_arrivals_size.v 2 additions, 2 deletionsanalysis/facts/periodic/task_arrivals_size.v
- analysis/facts/preemption/job/limited.v 1 addition, 1 deletionanalysis/facts/preemption/job/limited.v
- analysis/facts/preemption/job/nonpreemptive.v 3 additions, 3 deletionsanalysis/facts/preemption/job/nonpreemptive.v
- analysis/facts/preemption/job/preemptive.v 1 addition, 1 deletionanalysis/facts/preemption/job/preemptive.v
- analysis/facts/preemption/rtc_threshold/floating.v 2 additions, 2 deletionsanalysis/facts/preemption/rtc_threshold/floating.v
- analysis/facts/preemption/rtc_threshold/job_preemptable.v 2 additions, 2 deletionsanalysis/facts/preemption/rtc_threshold/job_preemptable.v
- analysis/facts/preemption/rtc_threshold/limited.v 1 addition, 1 deletionanalysis/facts/preemption/rtc_threshold/limited.v
- analysis/facts/preemption/rtc_threshold/nonpreemptive.v 1 addition, 1 deletionanalysis/facts/preemption/rtc_threshold/nonpreemptive.v
- analysis/facts/preemption/rtc_threshold/preemptive.v 2 additions, 2 deletionsanalysis/facts/preemption/rtc_threshold/preemptive.v
Loading
Please register or sign in to comment