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"