# HG changeset patch
# User wenzelm
# Date 1002204463 -7200
# Node ID cb64368fb4059c2902d23159ecb2f1902ca9b84c
# Parent  38788d98504f0a09bac472ef7e95c8b99921bd94
improved proof by cases and induction;

diff -r 38788d98504f -r cb64368fb405 NEWS
--- a/NEWS	Thu Oct 04 16:07:20 2001 +0200
+++ b/NEWS	Thu Oct 04 16:07:43 2001 +0200
@@ -16,17 +16,20 @@
 
 *** Isar ***
 
-* Isar/Pure: renamed "antecedent" case to "rule_context";
-
-* Isar/HOL: 'recdef' now fails on unfinished automated proofs, use
+* renamed "antecedent" case to "rule_context";
+
+* improved proof by cases and induction:
+  - moved induct/cases attributes to Pure;
+  - added 'print_induct_rules' (covered by help item in Proof General > 3.3);
+  - generic setup instantiated for FOL and HOL;
+  - removed obsolete "(simplified)" and "(stripped)" options;
+
+* HOL: 'recdef' now fails on unfinished automated proofs, use
 "(permissive)" option to recover old behavior;
 
-* Isar/HOL: 'inductive' now longer features separate (collective)
+* HOL: 'inductive' now longer features separate (collective)
 attributes for 'intros';
 
-* moved induct/cases attributes to Pure, added 'print_induct_rules'
-command;
-
 
 *** HOL ***