# HG changeset patch
# User paulson
# Date 835108667 -7200
# Node ID cd3ffa5f1e311c4048d1a138836dd7377a4842d7
# Parent  89f8d4a88cca201bc4ec500ed045f5324e7a87d9
Addition of setOfList

diff -r 89f8d4a88cca -r cd3ffa5f1e31 src/HOL/ex/SList.ML
--- a/src/HOL/ex/SList.ML	Tue Jun 18 16:36:04 1996 +0200
+++ b/src/HOL/ex/SList.ML	Tue Jun 18 16:37:47 1996 +0200
@@ -283,6 +283,7 @@
 val [ttl_Nil,ttl_Cons] = list_recs ttl_def;
 val [append_Nil3,append_Cons] = list_recs append_def;
 val [mem_Nil, mem_Cons] = list_recs mem_def;
+val [setOfList_Nil,setOfList_Cons] = list_recs setOfList_def;
 val [map_Nil,map_Cons] = list_recs map_def;
 val [list_case_Nil,list_case_Cons] = list_recs list_case_def;
 val [filter_Nil,filter_Cons] = list_recs filter_def;
@@ -292,6 +293,7 @@
    mem_Nil, mem_Cons,
    list_case_Nil, list_case_Cons,
    append_Nil3, append_Cons,
+   setOfList_Nil, setOfList_Cons, 
    map_Nil, map_Cons,
    filter_Nil, filter_Cons];
 
diff -r 89f8d4a88cca -r cd3ffa5f1e31 src/HOL/ex/SList.thy
--- a/src/HOL/ex/SList.thy	Tue Jun 18 16:36:04 1996 +0200
+++ b/src/HOL/ex/SList.thy	Tue Jun 18 16:37:47 1996 +0200
@@ -37,7 +37,8 @@
   null      :: 'a list => bool
   hd        :: 'a list => 'a
   tl,ttl    :: 'a list => 'a list
-  mem           :: ['a, 'a list] => bool                        (infixl 55)
+  setOfList :: ('a list => 'a set)
+  mem       :: ['a, 'a list] => bool                            (infixl 55)
   map       :: ('a=>'b) => ('a list => 'b list)
   "@"       :: ['a list, 'a list] => 'a list                    (infixr 65)
   filter    :: ['a => bool, 'a list] => 'a list
@@ -104,6 +105,8 @@
   (* a total version of tl: *)
   ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r.xs)"
 
+  setOfList_def "setOfList xs == list_rec xs {} (%x l r. insert x r)"
+
   mem_def       "x mem xs            == 
                    list_rec xs False (%y ys r. if y=x then True else r)"
   map_def       "map f xs            == list_rec xs [] (%x l r. f(x)#r)"