# HG changeset patch
# User nipkow
# Date 1101282221 -3600
# Node ID b8da286bb9ad35144ea7316490baee2c7092e11f
# Parent  e9669e0d6452225a19bd46f806092887d371b71e
*** empty log message ***

diff -r e9669e0d6452 -r b8da286bb9ad NEWS
--- 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"