# 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)"