src/Pure/library.ML
changeset 410 c8171ee32744
parent 380 daca5b594fb3
child 512 55755ed9fab9
     1.1 --- a/src/Pure/library.ML	Wed Jun 01 13:18:35 1994 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Jun 01 15:42:25 1994 +0200
     1.3 @@ -18,8 +18,8 @@
     1.4  fun K x y = x;
     1.5  
     1.6  (*reverse apply*)
     1.7 -infix also;
     1.8 -fun (x also f) = f x;
     1.9 +infix |>;
    1.10 +fun (x |> f) = f x;
    1.11  
    1.12  (*combine two functions forming the union of their domains*)
    1.13  infix orelf;