# HG changeset patch
# User wenzelm
# Date 1004459636 -3600
# Node ID 26b95a6f3f79c376e546fa482cb129d40d67f9f8
# Parent  06658189cd5138c753aaf91786fec427c919209e
- 'induct' method now derives symbolic cases from the *rulified* rule
(before it used to rulify cases stemming from the internal atomized
version); this means that the context of a non-atomic statement
becomes is included in the hypothesis, avoiding the slightly
cumbersome show "PROP ?case" form;

diff -r 06658189cd51 -r 26b95a6f3f79 NEWS
--- a/NEWS	Tue Oct 30 17:33:03 2001 +0100
+++ b/NEWS	Tue Oct 30 17:33:56 2001 +0100
@@ -33,14 +33,24 @@
 *** Isar ***
 
 * improved proof by cases and induction:
+
   - 'case' command admits impromptu naming of parameters (such as
-    "case (Suc n)");
+"case (Suc n)");
+
   - 'induct' method divinates rule instantiation from the inductive
-    claim; no longer requires excessive ?P bindings for proper
-    instantiation of cases;
+claim; no longer requires excessive ?P bindings for proper
+instantiation of cases;
+
   - 'induct' method properly enumerates all possibilities of set/type
-    rules; as a consequence facts may be also passed through *type*
-    rules without further ado;
+rules; as a consequence facts may be also passed through *type* rules
+without further ado;
+
+  - 'induct' method now derives symbolic cases from the *rulified*
+rule (before it used to rulify cases stemming from the internal
+atomized version); this means that the context of a non-atomic
+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;