# HG changeset patch
# User wenzelm
# Date 1004488024 -3600
# Node ID 4a622f5fb1640fa7db2f58d7a69f5d23060257cf
# Parent  319cc9aba0cf099c9c7a105cdc60d475e687ffa8
  - 'induct' may now use elim-style induction rules without chaining
facts, using ``missing'' premises from the goal state; this allows
rules stemming from inductive sets to be applied in unstructured
scripts, while still benefitting from proper handling of non-atomic
statements; NB: major inductive premises need to be put first, all the
rest of the goal is passed through the induction;

diff -r 319cc9aba0cf -r 4a622f5fb164 NEWS
--- a/NEWS	Wed Oct 31 01:26:42 2001 +0100
+++ b/NEWS	Wed Oct 31 01:27:04 2001 +0100
@@ -33,6 +33,10 @@
 *** Isar ***
 
 * improved proof by cases and induction:
+  - removed obsolete "(simplified)" and "(stripped)" options of methods;
+  - added 'print_induct_rules' (covered by help item in Proof General > 3.3);
+  - moved induct/cases attributes to Pure, methods to Provers;
+  - generic method setup instantiated for FOL and HOL;
 
   - 'case' command admits impromptu naming of parameters (such as
 "case (Suc n)");
@@ -51,10 +55,12 @@
 statement becomes is included in the hypothesis, avoiding the slightly
 cumbersome show "PROP ?case" form;
 
-  - removed obsolete "(simplified)" and "(stripped)" options of methods;
-  - added 'print_induct_rules' (covered by help item in Proof General > 3.3);
-  - moved induct/cases attributes to Pure, methods to Provers;
-  - generic method setup instantiated for FOL and HOL;
+  - 'induct' may now use elim-style induction rules without chaining
+facts, using ``missing'' premises from the goal state; this allows
+rules stemming from inductive sets to be applied in unstructured
+scripts, while still benefitting from proper handling of non-atomic
+statements; NB: major inductive premises need to be put first, all the
+rest of the goal is passed through the induction;
 
 * Pure: renamed "antecedent" case to "rule_context";