# HG changeset patch
# User wenzelm
# Date 1012069201 -3600
# Node ID de505273c971374d9de5fd4393f4279833664146
# Parent  c6a8e310aec55b829db5a8aa74d8cb3cd20fc3b6
Isar cases/induct: no backtracking;

diff -r c6a8e310aec5 -r de505273c971 NEWS
--- a/NEWS	Sat Jan 26 19:17:15 2002 +0100
+++ b/NEWS	Sat Jan 26 19:20:01 2002 +0100
@@ -59,6 +59,8 @@
   - 'induct' proper support for mutual induction involving non-atomic
     rule statements (uses the new concept of simultaneous goals, see
     below);
+  - append all possible rule selections, but only use the first
+    success (no backtracking);
   - removed obsolete "(simplified)" and "(stripped)" options of methods;
   - undeclared rule case names default to numbers 1, 2, 3, ...;
   - added 'print_induct_rules' (covered by help item in recent Proof