src/Pure/library.ML
changeset 410 c8171ee32744
parent 380 daca5b594fb3
child 512 55755ed9fab9
equal deleted inserted replaced
409:54fcef4db0db 410:c8171ee32744
    16 fun uncurry f (x, y) = f x y;
    16 fun uncurry f (x, y) = f x y;
    17 fun I x = x;
    17 fun I x = x;
    18 fun K x y = x;
    18 fun K x y = x;
    19 
    19 
    20 (*reverse apply*)
    20 (*reverse apply*)
    21 infix also;
    21 infix |>;
    22 fun (x also f) = f x;
    22 fun (x |> f) = f x;
    23 
    23 
    24 (*combine two functions forming the union of their domains*)
    24 (*combine two functions forming the union of their domains*)
    25 infix orelf;
    25 infix orelf;
    26 fun f orelf g = fn x => f x handle Match => g x;
    26 fun f orelf g = fn x => f x handle Match => g x;
    27 
    27