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

NEWS

changeset 15319 | b8da286bb9ad |

parent 15287 | 55b7f7920622 |

child 15350 | 53d2927d9680 |

--- a/NEWS Tue Nov 23 18:58:59 2004 +0100 +++ b/NEWS Wed Nov 24 08:43:41 2004 +0100 @@ -221,6 +221,9 @@ Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e' now translates into 'setsum' as above. +* HOL: Finite set induction: In Isar proofs, the insert case is now + "case (insert x F)" instead of the old counterintuitive "case (insert F x)". + * HOL/Simplifier: - Is now set up to reason about transitivity chains involving "trancl"