changeset 63415 | 8f91c2f447a0 |
parent 63377 | 64adf4ba9526 |
child 63462 | c1fe30f2bc32 |
--- a/src/HOL/Library/Combine_PER.thy Fri Jul 08 19:35:31 2016 +0200 +++ b/src/HOL/Library/Combine_PER.thy Fri Jul 08 23:43:11 2016 +0200 @@ -44,7 +44,7 @@ "transp R \<Longrightarrow> transp (combine_per P R)" by (auto intro!: transpI elim: transpE) -lemma equivp_combine_per_part_equivp: +lemma equivp_combine_per_part_equivp [intro?]: fixes R (infixl "\<approx>" 50) assumes "\<exists>x. P x" and "equivp R" shows "part_equivp (combine_per P R)"