changeset 44921 | 58eef4843641 |
parent 44890 | 22f665a2e91c |
child 45116 | f947eeef6b6f |
--- a/src/HOL/Transitive_Closure.thy Tue Sep 13 08:21:51 2011 -0700 +++ b/src/HOL/Transitive_Closure.thy Tue Sep 13 17:07:33 2011 -0700 @@ -220,7 +220,7 @@ apply (rename_tac a b) apply (case_tac "a = b") apply blast - apply (blast intro!: r_into_rtrancl) + apply blast done lemma rtranclp_r_diff_Id: "(inf r op ~=)^** = r^**"