| changeset 21115 | f4e79a09c305 |
| parent 21063 | 3c5074f028c8 |
| child 21125 | 9b7d35ca1eef |
--- a/src/HOL/Library/ExecutableSet.thy Tue Oct 31 09:28:57 2006 +0100 +++ b/src/HOL/Library/ExecutableSet.thy Tue Oct 31 09:29:01 2006 +0100 @@ -271,7 +271,7 @@ "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" .. code_abstype "'a set" "'a list" where - "{}" \<equiv> "empty_list" + "{}" \<equiv> empty_list insert \<equiv> insertl "op \<union>" \<equiv> unionl "op \<inter>" \<equiv> intersect