# HG changeset patch
# User haftmann
# Date 1468014191 -7200
# Node ID 8f91c2f447a0f338edcb0e8751b1cdd272a1dc21
# Parent  beb987127d0f2b3b6536ab9a0baaa3a884440b11
default rule for single-step reasoning

diff -r beb987127d0f -r 8f91c2f447a0 src/HOL/Library/Combine_PER.thy
--- 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)"