# HG changeset patch
# User haftmann
# Date 1748521028 -7200
# Node ID e63593ef8b15c61c97a9f7bcc19b80ed23f70fb6
# Parent  0faed76929b142f475f4271f4bd1468b47bc7591
annotate auxiliary operations explicitly

diff -r 0faed76929b1 -r e63593ef8b15 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu May 29 11:15:48 2025 +0200
+++ b/src/HOL/Set.thy	Thu May 29 14:17:08 2025 +0200
@@ -1884,13 +1884,13 @@
 context
 begin
 
-qualified definition is_empty :: "'a set \<Rightarrow> bool"
+qualified definition is_empty :: "'a set \<Rightarrow> bool" \<comment> \<open>only for code generation\<close>
   where is_empty_iff [code_abbrev, simp]: "is_empty A \<longleftrightarrow> A = {}"
 
-qualified definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
+qualified definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" \<comment> \<open>only for code generation\<close>
   where remove_eq [code_abbrev, simp]: "remove x A = A - {x}"
 
-qualified definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"
+qualified definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" \<comment> \<open>only for code generation\<close>
   where filter_eq [code_abbrev, simp]: "filter P A = {a \<in> A. P a}"
 
 end