--- a/NEWS Fri Sep 24 12:22:59 1999 +0200
+++ b/NEWS Fri Sep 24 15:28:12 1999 +0200
@@ -35,14 +35,15 @@
* Provers/Arith/fast_lin_arith.ML contains a functor for creating a
decision procedure for linear arithmetic. Currently it is used for
-types `nat' and `int' in HOL (see below) but can, should and will be
-instantiated for other types and logics as well.
+types `nat', `int', and `real' in HOL (see below); it can, should and
+will be instantiated for other types and logics as well.
* The simplifier now accepts rewrite rules with flexible heads, eg
hom ?f ==> ?f(?x+?y) = ?f ?x + ?f ?y
They are applied like any rule with a non-pattern lhs, i.e. by first-order
matching.
+
*** General ***
* new Isabelle/Isar subsystem provides an alternative to traditional
@@ -65,7 +66,8 @@
* theory loader rewritten from scratch (may not be fully
bug-compatible); old loadpath variable has been replaced by show_path,
add_path, del_path, reset_path functions; new operations such as
-update_thy, touch_thy, remove_thy (see also isatool doc ref);
+update_thy, touch_thy, remove_thy, use/update_thy_only (see also
+isatool doc ref);
* improved isatool install: option -k creates KDE application icon,
option -p DIR installs standalone binaries;
@@ -102,7 +104,12 @@
* function bind_thms stores lists of theorems (cf. bind_thm);
-* new shorthand tactics ftac, eatac, datac, fatac
+* new shorthand tactics ftac, eatac, datac, fatac;
+
+* qed (and friends) now accept "" as result name; in that case the
+result is not stored, but proper checks and presentation of the result
+still apply;
+
*** HOL ***