author | nipkow |
Wed, 24 Nov 2004 08:43:41 +0100 | |
changeset 15319 | b8da286bb9ad |
parent 15318 | e9669e0d6452 |
child 15320 | dfc2654eea9f |
--- 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"