equal
deleted
inserted
replaced
139 "exhaustive_set f i = (if i = 0 then None else (f {} orelse exhaustive_set (%A. f A orelse exhaustive (%x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1)))" |
139 "exhaustive_set f i = (if i = 0 then None else (f {} orelse exhaustive_set (%A. f A orelse exhaustive (%x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1)))" |
140 |
140 |
141 instance .. |
141 instance .. |
142 |
142 |
143 end |
143 end |
144 |
|
145 definition (in term_syntax) [code_unfold]: "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)" |
|
146 definition (in term_syntax) [code_unfold]: "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s" |
|
147 |
144 |
148 instantiation set :: (full_exhaustive) full_exhaustive |
145 instantiation set :: (full_exhaustive) full_exhaustive |
149 begin |
146 begin |
150 |
147 |
151 fun full_exhaustive_set |
148 fun full_exhaustive_set |