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/Lifting_Set.thy
changeset 62343 24106dc44def
parent 61952 546958347e05
child 63040 eb4ddd18d635 
--- a/src/HOL/Lifting_Set.thy	Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Lifting_Set.thy	Wed Feb 17 21:51:56 2016 +0100
@@ -138,7 +138,7 @@
 
 lemma UNION_transfer [transfer_rule]:
   "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
-  unfolding Union_image_eq [symmetric, abs_def] by transfer_prover
+  by transfer_prover
 
 lemma Ball_transfer [transfer_rule]:
   "(rel_set A ===> (A ===> op =) ===> op =) Ball Ball"
@@ -176,11 +176,11 @@
 
 lemma INF_parametric [transfer_rule]:
   "(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) INFIMUM INFIMUM"
-  unfolding INF_def [abs_def] by transfer_prover
+  by transfer_prover
 
 lemma SUP_parametric [transfer_rule]:
   "(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) SUPREMUM SUPREMUM"
-  unfolding SUP_def [abs_def] by transfer_prover
+  by transfer_prover
 
 
 subsubsection \<open>Rules requiring bi-unique, bi-total or right-total relations\<close>
isabelle