* Pure: improved error reporting of simprocs;
authorwenzelm
Thu Aug 08 23:42:10 2002 +0200 (2002-08-08)
changeset 134789cfbcb9acfef
parent 13477 6f9111705d4f
child 13479 7123ae179212
* Pure: improved error reporting of simprocs;
tuned;
NEWS
     1.1 --- a/NEWS	Wed Aug 07 20:11:07 2002 +0200
     1.2 +++ b/NEWS	Thu Aug 08 23:42:10 2002 +0200
     1.3 @@ -29,9 +29,6 @@
     1.4  "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from
     1.5  the goal statement); "foo" still refers to all facts collectively;
     1.6  
     1.7 -* Provers: Simplifier.simproc(_i) now provide sane interface for
     1.8 -setting up simprocs;
     1.9 -
    1.10  
    1.11  *** HOL ***
    1.12  
    1.13 @@ -54,6 +51,18 @@
    1.14  takes ~= in premises into account (by performing a case split);
    1.15  
    1.16  
    1.17 +*** ML ***
    1.18 +
    1.19 +* Pure: Tactic.prove provides sane interface for internal proofs;
    1.20 +omits the infamous "standard" operation, so this is more appropriate
    1.21 +than prove_goalw_cterm in many situations (e.g. in simprocs);
    1.22 +
    1.23 +* Pure: improved error reporting of simprocs;
    1.24 +
    1.25 +* Provers: Simplifier.simproc(_i) provides sane interface for setting
    1.26 +up simprocs;
    1.27 +
    1.28 +
    1.29  
    1.30  New in Isabelle2002 (March 2002)
    1.31  --------------------------------