*** empty log message ***
authornipkow
Wed Nov 24 08:43:41 2004 +0100 (2004-11-24)
changeset 15319b8da286bb9ad
parent 15318 e9669e0d6452
child 15320 dfc2654eea9f
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Tue Nov 23 18:58:59 2004 +0100
     1.2 +++ b/NEWS	Wed Nov 24 08:43:41 2004 +0100
     1.3 @@ -221,6 +221,9 @@
     1.4    Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e'
     1.5    now translates into 'setsum' as above.
     1.6  
     1.7 +* HOL: Finite set induction: In Isar proofs, the insert case is now
     1.8 +  "case (insert x F)" instead of the old counterintuitive "case (insert F x)".
     1.9 +
    1.10  * HOL/Simplifier:
    1.11  
    1.12    - Is now set up to reason about transitivity chains involving "trancl"