src/Pure/library.ML
changeset 14981 e73f8140af78
parent 14968 9db3d2be8cdf
child 15035 8c57751cd43f
equal deleted inserted replaced
14980:267cc670317a 14981:e73f8140af78
     1 (*  Title:      Pure/library.ML
     1 (*  Title:      Pure/library.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Author:     Markus Wenzel, TU Munich
     4     Author:     Markus Wenzel, TU Munich
     5     License:    GPL (GNU GENERAL PUBLIC LICENSE)
       
     6 
     5 
     7 Basic library: functions, options, pairs, booleans, lists, integers,
     6 Basic library: functions, options, pairs, booleans, lists, integers,
     8 rational numbers, strings, lists as sets, association lists, generic
     7 rational numbers, strings, lists as sets, association lists, generic
     9 tables, balanced trees, orders, current directory, misc.
     8 tables, balanced trees, orders, current directory, misc.
    10 *)
     9 *)