summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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 |