NEWS
changeset 13425 119ae829ad9b
parent 13410 f2cd09766864
child 13443 1c3327c348b3
     1.1 --- a/NEWS	Fri Jul 26 21:07:57 2002 +0200
     1.2 +++ b/NEWS	Fri Jul 26 21:09:39 2002 +0200
     1.3 @@ -15,6 +15,10 @@
     1.4  context; potential INCOMPATIBILITY, use "(open)" option to fall back
     1.5  on the old view without predicates;
     1.6  
     1.7 +* improved induct method: assumptions introduced by case "foo" are
     1.8 +split into "foo.hyps" (from the rule) and "foo.prems" (from the goal
     1.9 +statement); "foo" still refers to all facts collectively;
    1.10 +
    1.11  * improved thms_containing: proper indexing of facts instead of raw
    1.12  theorems; check validity of results wrt. current name space; include
    1.13  local facts of proof configuration (also covers active locales); an