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

NEWS

changeset 19034 | db16746a5604 |

parent 19032 | d25dfb797612 |

child 19081 | 085b5badb8de |

equal
deleted
inserted
replaced

19033:24e251657e56 | 19034:db16746a5604 |
---|---|

361 mangling (bijective mapping from any expression values to strings). |
361 mangling (bijective mapping from any expression values to strings). |

362 |
362 |

363 * Pure/General/rat.ML implements rational numbers. |
363 * Pure/General/rat.ML implements rational numbers. |

364 |
364 |

365 * Pure/General/table.ML: the join operations now works via exceptions |
365 * Pure/General/table.ML: the join operations now works via exceptions |

366 DUP/SAME instead of type option. This is simpler in simple cases, and |
366 DUP/SAME instead of type option. This is both simpler and admits |

367 admits slightly more efficient complex applications. |
367 slightly more efficient complex applications. |

368 |
368 |

369 * Pure: datatype Context.generic joins theory/Proof.context and |
369 * Pure: datatype Context.generic joins theory/Proof.context and |

370 provides some facilities for code that works in either kind of |
370 provides some facilities for code that works in either kind of |

371 context, notably GenericDataFun for uniform theory and proof data. |
371 context, notably GenericDataFun for uniform theory and proof data. |

372 |
372 |