| changeset 16690 | b8b2579a2509 |
| parent 16689 | 05b986733a59 |
| child 16717 | 710a7a7a2b65 |
--- a/NEWS Tue Jul 05 14:07:08 2005 +0200 +++ b/NEWS Tue Jul 05 15:39:48 2005 +0200 @@ -416,7 +416,7 @@ the runtime). * Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a -reasonably efficient light-weight implementation of lists as sets. +reasonably efficient light-weight implementation of sets as lists. * Pure: more efficient orders for basic syntactic entities: added fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord