set_of_list -> set
authornipkow
Thu Jul 03 13:44:54 1997 +0200 (1997-07-03)
changeset 348762a6a08471e4
parent 3486 10cf84e5d2c2
child 3488 32f90fe0f3f9
set_of_list -> set
doc-src/Logics/HOL.tex
     1.1 --- a/doc-src/Logics/HOL.tex	Wed Jul 02 16:53:14 1997 +0200
     1.2 +++ b/doc-src/Logics/HOL.tex	Thu Jul 03 13:44:54 1997 +0200
     1.3 @@ -1285,7 +1285,7 @@
     1.4          & & mapping functional\\
     1.5    \cdx{filter}  & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
     1.6          & & filter functional\\
     1.7 -  \cdx{set_of_list}& $\alpha\,list \To \alpha\,set$ & & elements\\
     1.8 +  \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\
     1.9    \sdx{mem}  & $[\alpha,\alpha\,list]\To bool$    &  Left 55   & membership\\
    1.10    \cdx{foldl}   & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &
    1.11    & iteration \\
    1.12 @@ -1333,8 +1333,8 @@
    1.13  filter P [] = []
    1.14  filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
    1.15  
    1.16 -set_of_list [] = \ttlbrace\ttrbrace
    1.17 -set_of_list (x#xs) = insert x (set_of_list xs)
    1.18 +set [] = \ttlbrace\ttrbrace
    1.19 +set (x#xs) = insert x (set xs)
    1.20  
    1.21  x mem [] = False
    1.22  x mem (y#ys) = (if y=x then True else x mem ys)