Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BNF/Equiv_Relations_More.thy
changeset 54483 9f24325c2550
parent 49510 ba50d204095e 
--- a/src/HOL/BNF/Equiv_Relations_More.thy	Tue Nov 19 01:29:50 2013 +0100
+++ b/src/HOL/BNF/Equiv_Relations_More.thy	Tue Nov 19 01:29:50 2013 +0100
@@ -59,7 +59,7 @@
 
 lemma in_quotient_imp_in_rel:
 "\<lbrakk>equiv A r; X \<in> A//r; {x,y} \<subseteq> X\<rbrakk> \<Longrightarrow> (x,y) \<in> r"
-using quotient_eq_iff by fastforce
+using quotient_eq_iff[THEN iffD1] by fastforce
 
 lemma in_quotient_imp_closed:
 "\<lbrakk>equiv A r; X \<in> A//r; x \<in> X; (x,y) \<in> r\<rbrakk> \<Longrightarrow> y \<in> X"
isabelle