This MR 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]
@proux @bbb, what do you think?