# HG changeset patch
# User desharna
# Date 1685223160 -7200
# Node ID 84a7a0029c82b80e82faa73b7880921c46905032
# Parent  7735645667f02287c97db3e8a1dfc7c893a1bbf5
set up code generation for fset

diff -r 7735645667f0 -r 84a7a0029c82 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Fri May 26 15:44:59 2023 +0200
+++ b/src/HOL/Library/FSet.thy	Sat May 27 23:32:40 2023 +0200
@@ -1970,4 +1970,22 @@
 
 end
 
+
+subsection \<open>Code Generation Setup\<close>
+
+text \<open>The following @{attribute code_unfold} lemmas are so the pre-processor of the code generator
+will perform conversions like, e.g.,
+@{lemma "x |\<in>| fimage f (fset_of_list xs) \<longleftrightarrow> x \<in> f ` set xs"
+  by (simp only: fimage.rep_eq fset_of_list.rep_eq)}.\<close>
+
+declare
+  ffilter.rep_eq[code_unfold]
+  fimage.rep_eq[code_unfold]
+  finsert.rep_eq[code_unfold]
+  fset_of_list.rep_eq[code_unfold]
+  inf_fset.rep_eq[code_unfold]
+  minus_fset.rep_eq[code_unfold]
+  sup_fset.rep_eq[code_unfold]
+  uminus_fset.rep_eq[code_unfold]
+
 end