src/Pure/Concurrent/par_list_dummy.ML
changeset 28556 85d2972fe9e6
parent 28546 d57bfb44c9e5
child 29368 503ce3f8f092
equal deleted inserted replaced
28555:d59712ee942c 28556:85d2972fe9e6
     8 structure ParList: PAR_LIST =
     8 structure ParList: PAR_LIST =
     9 struct
     9 struct
    10 
    10 
    11 val map = map;
    11 val map = map;
    12 val get_some = get_first;
    12 val get_some = get_first;
    13 val fins_some = find_first;
    13 val find_some = find_first;
    14 val exists = exists;
    14 val exists = exists;
    15 val forall = forall;
    15 val forall = forall;
    16 
    16 
    17 end;
    17 end;