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/Quotient_Examples/Lift_FSet.thy
changeset 47676 ec235f564444
parent 47660 7a5c681c0265
child 47937 70375fa2679d 
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Sun Apr 22 16:53:24 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Sun Apr 22 17:54:47 2012 +0200
@@ -156,7 +156,7 @@
   apply (elim relcomppE)
   apply (rule relcomppI)
   apply (erule (1) map_transfer [THEN fun_relD, THEN fun_relD])
-  apply (erule fmap.transfer [THEN fun_relD, THEN fun_relD, OF refl])
+  apply (erule fmap.transfer [THEN fun_relD, THEN fun_relD, unfolded relator_eq, OF refl])
   done
 
 lemma ffilter_transfer [transfer_rule]:
@@ -166,7 +166,7 @@
   apply (elim relcomppE)
   apply (rule relcomppI)
   apply (erule (1) filter_transfer [THEN fun_relD, THEN fun_relD])
-  apply (erule ffilter.transfer [THEN fun_relD, THEN fun_relD, OF refl])
+  apply (erule ffilter.transfer [THEN fun_relD, THEN fun_relD, unfolded relator_eq, OF refl])
   done
 
 lemma fset_transfer [transfer_rule]:
@@ -174,7 +174,7 @@
   unfolding cr_fset'_def
   apply (intro fun_relI)
   apply (elim relcomppE)
-  apply (drule fset.transfer [THEN fun_relD])
+  apply (drule fset.transfer [THEN fun_relD, unfolded relator_eq])
   apply (erule subst)
   apply (erule set_transfer [THEN fun_relD])
   done
isabelle