I added lexn_transI.
Thanks
Tobias
On 30/12/2015 15:25, Mathias Fleury wrote:
Dear list,
I stumbled upon some lemmas that have a counterpart in Isabelle (like
rtranclp_mono vs tranclp_mono), but are not included. Is there a reason why the
following lemmas are not included in Isabelle?
rtrancl
Dear list,
I stumbled upon some lemmas that have a counterpart in Isabelle (like
rtranclp_mono vs tranclp_mono), but are not included. Is there a reason why the
following lemmas are not included in Isabelle?
rtranclp vs tranclp:
there is a rtranclp_mono "r ≤ s ==> r^** ≤ s^**", but no tranclp_
