tuned;
authorwenzelm
Fri Sep 24 15:28:12 1999 +0200 (1999-09-24 ago)
changeset 75936bc8fa8b4b24
parent 7592 c29a222cf981
child 7594 8a188ef6545e
tuned;
NEWS
     1.1 --- a/NEWS	Fri Sep 24 12:22:59 1999 +0200
     1.2 +++ b/NEWS	Fri Sep 24 15:28:12 1999 +0200
     1.3 @@ -35,14 +35,15 @@
     1.4  
     1.5  * Provers/Arith/fast_lin_arith.ML contains a functor for creating a
     1.6  decision procedure for linear arithmetic. Currently it is used for
     1.7 -types `nat' and `int' in HOL (see below) but can, should and will be
     1.8 -instantiated for other types and logics as well.
     1.9 +types `nat', `int', and `real' in HOL (see below); it can, should and
    1.10 +will be instantiated for other types and logics as well.
    1.11  
    1.12  * The simplifier now accepts rewrite rules with flexible heads, eg
    1.13       hom ?f ==> ?f(?x+?y) = ?f ?x + ?f ?y
    1.14    They are applied like any rule with a non-pattern lhs, i.e. by first-order
    1.15    matching.
    1.16  
    1.17 +
    1.18  *** General ***
    1.19  
    1.20  * new Isabelle/Isar subsystem provides an alternative to traditional
    1.21 @@ -65,7 +66,8 @@
    1.22  * theory loader rewritten from scratch (may not be fully
    1.23  bug-compatible); old loadpath variable has been replaced by show_path,
    1.24  add_path, del_path, reset_path functions; new operations such as
    1.25 -update_thy, touch_thy, remove_thy (see also isatool doc ref);
    1.26 +update_thy, touch_thy, remove_thy, use/update_thy_only (see also
    1.27 +isatool doc ref);
    1.28  
    1.29  * improved isatool install: option -k creates KDE application icon,
    1.30  option -p DIR installs standalone binaries;
    1.31 @@ -102,7 +104,12 @@
    1.32  
    1.33  * function bind_thms stores lists of theorems (cf. bind_thm);
    1.34  
    1.35 -* new shorthand tactics ftac, eatac, datac, fatac
    1.36 +* new shorthand tactics ftac, eatac, datac, fatac;
    1.37 +
    1.38 +* qed (and friends) now accept "" as result name; in that case the
    1.39 +result is not stored, but proper checks and presentation of the result
    1.40 +still apply;
    1.41 +
    1.42  
    1.43  *** HOL ***
    1.44