# HG changeset patch
# User nipkow
# Date 867930294 -7200
# Node ID 62a6a08471e4739a04e9f1804dedf05ce1a81bdb
# Parent  10cf84e5d2c272fe62f19d0abf6e0ea8eb8fae8b
set_of_list -> set

diff -r 10cf84e5d2c2 -r 62a6a08471e4 doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Wed Jul 02 16:53:14 1997 +0200
+++ b/doc-src/Logics/HOL.tex	Thu Jul 03 13:44:54 1997 +0200
@@ -1285,7 +1285,7 @@
         & & mapping functional\\
   \cdx{filter}  & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
         & & filter functional\\
-  \cdx{set_of_list}& $\alpha\,list \To \alpha\,set$ & & elements\\
+  \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\
   \sdx{mem}  & $[\alpha,\alpha\,list]\To bool$    &  Left 55   & membership\\
   \cdx{foldl}   & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &
   & iteration \\
@@ -1333,8 +1333,8 @@
 filter P [] = []
 filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
 
-set_of_list [] = \ttlbrace\ttrbrace
-set_of_list (x#xs) = insert x (set_of_list xs)
+set [] = \ttlbrace\ttrbrace
+set (x#xs) = insert x (set xs)
 
 x mem [] = False
 x mem (y#ys) = (if y=x then True else x mem ys)