--- a/NEWS Tue Aug 01 11:58:27 2000 +0200
+++ b/NEWS Tue Aug 01 13:41:23 2000 +0200
@@ -25,15 +25,17 @@
* HOL: exhaust_tac on datatypes superceded by new generic case_tac;
-* HOL: simplification no longer dives into case-expressions
+* HOL: simplification no longer dives into case-expressions;
* HOL: the recursion equations generated by 'recdef' are now called
f.simps instead of f.rules;
-* HOL: theory Sexp now in HOL/Induct examples (used to be part of main
-HOL, but was unused); should better use HOL's datatype package anyway;
+* HOL: theory Sexp now in HOL/Induct examples (it used to be part of
+main HOL, but was unused); should better use HOL's datatype package
+anyway;
-* HOL: removed obsolete theorem binding expand_if, use split_if instead;
+* HOL: removed obsolete theorem binding expand_if (refer to split_if
+instead);
* HOL/Real: "rabs" replaced by overloaded "abs" function;
@@ -44,12 +46,12 @@
* HOL, ZF: syntax for quotienting wrt an equivalence relation changed from
A/r to A//r;
-* Isar: changed syntax of local blocks from {{ }} to { };
-
* Isar/Provers: intro/elim/dest attributes: changed
intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one
should have to change intro!! to intro? only);
+* Isar: changed syntax of local blocks from {{ }} to { };
+
* Provers: strengthened force_tac by using new first_best_tac;
* Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g.
@@ -97,6 +99,9 @@
on WWW server seperately); improved graphs of nested sessions; removed
graph for 'all sessions';
+* several improvements in isabelle.sty; \isamarkupheader is now
+\section by default;
+
*** Isar ***
@@ -104,11 +109,11 @@
to Hindley-Milner polymorphism (similar to ML); this accommodates
incremental type-inference nicely;
-* Pure: new 'obtain' language element supports generalized existence
-reasoning;
+* Pure: new derived language element 'obtain' supports generalized
+existence reasoning;
* Pure: new calculational elements 'moreover' and 'ultimately' support
-plain accumulation of results, without applying any rules yet;
+accumulation of results, without applying any rules yet;
* Pure: scalable support for case-analysis type proofs: new 'case'
language element refers to local contexts symbolically, as produced by
@@ -123,7 +128,7 @@
* Pure: changed syntax of local blocks from {{ }} to { };
-* Pure: syntax of sorts made inner, i.e. have to write "{a, b, c}"
+* Pure: syntax of sorts made 'inner', i.e. have to write "{a, b, c}"
instead of {a, b, c};
* Pure now provides its own version of intro/elim/dest attributes;
@@ -151,7 +156,7 @@
method anyway;
* HOL/Calculation: new rules for substitution in inequalities
-(monotonicity conditions are extracted to be proven terminally);
+(monotonicity conditions are extracted to be proven at end);
* HOL: removed obsolete expand_if = split_if; theorems if_splits =
split_if split_if_asm; datatype package provides theorems foo.splits =
@@ -189,7 +194,7 @@
*** HOL ***
-* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog
+* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog;
* HOL/Algebra: new theory of rings and univariate polynomials, by
Clemens Ballarin;
@@ -202,7 +207,7 @@
* HOL/ex/Multiquote: multiple nested quotations and anti-quotations --
basically a generalized version of de-Bruijn representation; very
-useful in avoiding lifting all operations;
+useful in avoiding lifting of operations;
* HOL/Real: "rabs" replaced by overloaded "abs" function;
@@ -237,18 +242,18 @@
individually as well, resulting in a separate list of theorems for
each equation;
-* HOL/While is a new theory that provides a while-combinator. It permits the
-definition of tail-recursive functions without the provision of a termination
-measure. The latter is necessary once the invariant proof rule for while is
-applied.
+* HOL/While is a new theory that provides a while-combinator. It
+permits the definition of tail-recursive functions without the
+provision of a termination measure. The latter is necessary once the
+invariant proof rule for while is applied.
* HOL: new (overloaded) notation for the set of elements below/above some
element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval.
* HOL: theorems impI, allI, ballI bound as "strip";
-* theory Sexp now in HOL/Induct examples (used to be part of main HOL,
-but was unused);
+* theory Sexp now in HOL/Induct examples (it used to be part of main
+HOL, but was unused);
* fewer consts declared as global (e.g. have to refer to "Lfp.lfp"
instead of "lfp" internally; affects ML packages only);
@@ -260,11 +265,14 @@
*** FOL & ZF ***
* AddIffs now available, giving theorems of the form P<->Q to the
- simplifier and classical reasoner simultaneously;
+simplifier and classical reasoner simultaneously;
*** General ***
+* blast(_tac) now handles actual object-logic rules as assumptions;
+note that auto(_tac) uses blast(_tac) internally, too;
+
* AST translation rules no longer require constant head on LHS;
* improved name spaces: ambiguous output is qualified; support for