Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
default rule for single-step reasoning
authorhaftmann
Fri, 08 Jul 2016 23:43:11 +0200
changeset 63415 8f91c2f447a0
parent 63414 beb987127d0f
child 63416 6af79184bef3
default rule for single-step reasoning
src/HOL/Library/Combine_PER.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle