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/Set.thy
changeset 82675 0a3d61228714
parent 82669 92afc125f7cd 
--- a/src/HOL/Set.thy	Sat May 31 21:51:08 2025 +0200
+++ b/src/HOL/Set.thy	Sun Jun 01 10:29:45 2025 +0200
@@ -17,7 +17,7 @@
 axiomatization Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" \<comment> \<open>comprehension\<close>
   and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" \<comment> \<open>membership\<close>
   where mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
-    and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
+    and Collect_mem_eq [simp, code_unfold]: "Collect (\<lambda>x. member x A) = A"
 
 notation
   member  (\<open>'(\<in>')\<close>) and
isabelle