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/Library/FSet.thy
changeset 82664 e9f3b94eb6a0
parent 81545 6f8a56a6b391 
--- a/src/HOL/Library/FSet.thy	Sat May 24 09:06:26 2025 +0200
+++ b/src/HOL/Library/FSet.thy	Wed May 28 17:49:22 2025 +0200
@@ -256,7 +256,7 @@
   by transfer_prover
 
 lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter
-  parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp
+  parametric Lifting_Set.filter_transfer by simp
 
 lift_definition fPow :: "'a fset \<Rightarrow> 'a fset fset" is Pow parametric Pow_transfer
 by (simp add: finite_subset)
@@ -1015,7 +1015,7 @@
   by (rule bind_const[Transfer.transferred])
 
 lemma ffmember_filter[simp]: "(x |\<in>| ffilter P A) = (x |\<in>| A \<and> P x)"
-  by (rule member_filter[Transfer.transferred])
+  by transfer simp
 
 lemma fequalityI: "A |\<subseteq>| B \<Longrightarrow> B |\<subseteq>| A \<Longrightarrow> A = B"
   by (rule equalityI[Transfer.transferred])
@@ -1112,7 +1112,7 @@
 
 lemma fset_of_list_filter[simp]:
   "fset_of_list (filter P xs) = ffilter P (fset_of_list xs)"
-  by transfer (auto simp: Set.filter_def)
+  by transfer auto
 
 lemma fset_of_list_subset[intro]:
   "set xs \<subseteq> set ys \<Longrightarrow> fset_of_list xs |\<subseteq>| fset_of_list ys"
isabelle