| changeset 21125 | 9b7d35ca1eef |
| parent 21115 | f4e79a09c305 |
| child 21153 | 8288c8f203de |
--- a/src/HOL/Library/ExecutableSet.thy Tue Oct 31 09:29:18 2006 +0100 +++ b/src/HOL/Library/ExecutableSet.thy Tue Oct 31 14:58:12 2006 +0100 @@ -285,7 +285,7 @@ Bex \<equiv> Blex code_gen "{}" insert "op \<union>" "op \<inter>" "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" - image Union Inter UNION INTER Ball Bex (SML -) + image Union Inter UNION INTER Ball Bex (SML *) subsection {* type serializations *}