src/Pure/library.ML
changeset 2403 8115988ccc22
parent 2317 672015b535d7
child 2471 09634c9cbf3c
equal deleted inserted replaced
2402:b3d273ce5601 2403:8115988ccc22
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 Basic library: functions, options, pairs, booleans, lists, integers,
     6 Basic library: functions, options, pairs, booleans, lists, integers,
     7 strings, lists as sets, association lists, generic tables, balanced trees,
     7 strings, lists as sets, association lists, generic tables, balanced trees,
     8 input / TextIO.output, timing, filenames, misc functions.
     8 input / output, timing, filenames, misc functions.
     9 *)
     9 *)
    10 
    10 
    11 infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
    11 infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
    12       mem mem_int mem_string union union_int union_string  
    12       mem mem_int mem_string union union_int union_string  
    13       inter inter_int inter_string subset subset_int subset_string subdir_of;
    13       inter inter_int inter_string subset subset_int subset_string subdir_of;