# HG changeset patch
# User wenzelm
# Date 1213118114 -7200
# Node ID 63d92a5e3784dd83ad0473fcb01fade481d97ff4
# Parent  38367dbccae55150c25d6f96e50f58164feb2896
proper news header;
methods case_tac and induct_tac now refer to usual declarations;
removed obsolete induct_tac and thm_induct_tac;

diff -r 38367dbccae5 -r 63d92a5e3784 NEWS
--- a/NEWS	Tue Jun 10 16:43:26 2008 +0200
+++ b/NEWS	Tue Jun 10 19:15:14 2008 +0200
@@ -1,39 +1,46 @@
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
-New
----
+New in this Isabelle version
+----------------------------
 
 *** Pure ***
 
-* 'instance': attached definitions now longer accepted.  INCOMPATIBILITY.
+* Command 'instance': attached definitions now longer accepted.
+INCOMPATIBILITY.
 
 * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
 
 
 *** HOL ***
 
-* 'rep_datatype': instead of theorem names the command now takes a list of terms
-denoting the constructors of the type to be represented as datatype.  The
-characteristic theorems have to be proven.  INCOMPATIBILITY.  Also observe that
-the following theorems have disappeared in favour of existing ones:
+* Methods "case_tac" and "induct_tac" now refer to the very same rule
+declarations as the structured Isar versions "cases" and "induct", cf.
+the corresponding "cases" and "induct" attributes.  INCOMPATIBILITY,
+in rare situations a different rule is selected --- notably nested
+tuple elimination instead of former prod.exhaust: use explicit
+(case_tac t rule: prod.exhaust) here.
+
+* Removed fact "case_split_thm", which duplicates "case_split".
+
+* Command 'rep_datatype': instead of theorem names the command now
+takes a list of terms denoting the constructors of the type to be
+represented as datatype.  The characteristic theorems have to be
+proven.  INCOMPATIBILITY.  Also observe that the following theorems
+have disappeared in favour of existing ones:
+
     unit_induct                 ~> unit.induct
     prod_induct                 ~> prod.induct
     sum_induct                  ~> sum.induct
     Suc_Suc_eq                  ~> nat.inject
     Suc_not_Zero Zero_not_Suc   ~> nat.distinct
 
-* Tactics induct_tac and thm_induct_tac now take explicit context as arguments;
-type-specific induction rules are identified by the 'induct' attribute rather
-than querying the datatype package directly.  INCOMPATIBILITY.
-
 * 'Least' operator now restricted to class 'order' (and subclasses).
 INCOMPATIBILITY.
 
-* Library/Nat_Infinity: added addition, numeral syntax and more instantiations
-for algebraic structures.  Removed some duplicate theorems.  Changes in simp
-rules.  INCOMPATIBILITY.
-
+* Library/Nat_Infinity: added addition, numeral syntax and more
+instantiations for algebraic structures.  Removed some duplicate
+theorems.  Changes in simp rules.  INCOMPATIBILITY.
 
 
 New in Isabelle2008 (June 2008)