Theory More_Abstract_Rewriting

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2017)
License: LGPL (see file COPYING.LESSER)
*)
theory More_Abstract_Rewriting
  imports "$AFP/Abstract_Rewriting/Abstract_Rewriting"
begin

section ‹Results that belong to @‹theory Abstract_Rewriting››

(*TODO: move*)
lemma rtrancl_eq_CR:
  assumes "r⇧* = s⇧*"
  shows "CR r ⟷ CR s"
  using assms by (auto simp: CR_defs join_def rtrancl_converse)

end