* Provers: Simplifier.simproc(_i) now provide sane interface for
authorwenzelm
Tue Aug 06 11:24:27 2002 +0200 (2002-08-06)
changeset 1346307747943c626
parent 13462 56610e2ba220
child 13464 c98321b8d638
* Provers: Simplifier.simproc(_i) now provide sane interface for
setting up simprocs;
NEWS
     1.1 --- a/NEWS	Tue Aug 06 11:22:05 2002 +0200
     1.2 +++ b/NEWS	Tue Aug 06 11:24:27 2002 +0200
     1.3 @@ -19,15 +19,18 @@
     1.4  parameters (as in CASL, for example); just specify something like
     1.5  ``var x + var y + struct M'' as import;
     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
    1.14 -optional limit for the number of printed facts may be given (the
    1.15 -default is 40);
    1.16 +* Pure: improved thms_containing: proper indexing of facts instead of
    1.17 +raw theorems; check validity of results wrt. current name space;
    1.18 +include local facts of proof configuration (also covers active
    1.19 +locales); an optional limit for the number of printed facts may be
    1.20 +given (the default is 40);
    1.21 +
    1.22 +* Provers: improved induct method: assumptions introduced by case
    1.23 +"foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from
    1.24 +the goal statement); "foo" still refers to all facts collectively;
    1.25 +
    1.26 +* Provers: Simplifier.simproc(_i) now provide sane interface for
    1.27 +setting up simprocs;
    1.28  
    1.29  
    1.30  *** HOL ***