Dear all, how about adding the following lemmas to the order class?
lemma (in order) rtranclp_less_eq [simp]: "(op ≤)⇧*⇧* = op ≤" by (intro ext) (auto elim: rtranclp_induct) lemma (in order) tranclp_less [simp]: "(op <)⇧+⇧+ = op <" by (intro ext) (auto elim: tranclp_induct) lemma (in order) rtranclp_greater_eq [simp]: "(op ≥)⇧*⇧* = op ≥" by (intro ext) (auto elim: rtranclp_induct) lemma (in order) tranclp_greater [simp]: "(op >)⇧+⇧+ = op >" by (intro ext) (auto elim: tranclp_induct) cheers chris _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
