[isabelle-dev] new lemmas for Transitive_Closure + renaming

[Christian Sternagel]

Dear all,

I suggest to add the following lemmas to Transitive_Closure and the 
simplifier (I just copied the unicode-tokens from Isabelle/jEdit... I 
hope what arrives after emailing is the same what I sent):

lemma
   reflcl_idemp [simp]: "(R⇧=)⇧= = R⇧=" and
   reflclp_idemp [simp]: "(P⇧=⇧=)⇧=⇧= = P⇧=⇧="
   by blast+

Plus, for consistency, the following lemmas should be renamed:

   reflcl_tranclp ~> reflclp_tranclp
   rtranclp_reflcl ~> rtranclp_reflclp

and maybe

   reflcl_set_eq ~> reflclp_reflcl_conv

What do you think?

cheers

chris