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

NEWS

changeset 30300 | aa44d67eea16 |

parent 30298 | abefe1dfadbb |

child 30308 | 23935abfb549 |

equal
deleted
inserted
replaced

30299:51797bcf4fd1 | 30300:aa44d67eea16 |
---|---|

220 |
220 |

221 *** HOL *** |
221 *** HOL *** |

222 |
222 |

223 * New predicate "strict_mono" classifies strict functions on partial orders. |
223 * New predicate "strict_mono" classifies strict functions on partial orders. |

224 With strict functions on linear orders, reasoning about (in)equalities is |
224 With strict functions on linear orders, reasoning about (in)equalities is |

225 facilitated by theorems "strict_mono_eq", "strict_mono_eq" and "strict_mono_eq". |
225 facilitated by theorems "strict_mono_eq", "strict_mono_less_eq" and "strict_mono_less". |

226 |
226 |

227 * Auxiliary class "itself" has disappeared -- classes without any parameter |
227 * Auxiliary class "itself" has disappeared -- classes without any parameter |

228 are treated as expected by the 'class' command. |
228 are treated as expected by the 'class' command. |

229 |
229 |

230 * Leibnitz's Series for Pi and the arcus tangens and logarithm series. |
230 * Leibnitz's Series for Pi and the arcus tangens and logarithm series. |