# HG changeset patch
# User wenzelm
# Date 965130083 -7200
# Node ID aa757b35b129ab2a86a4ab9ba06f62965bab41b8
# Parent  f11bece4e2db06d16cc248f644cf5a497cea36af
* blast(_tac) now handles actual object-logic rules as assumptions;
note that auto(_tac) uses blast(_tac) internally, too;
tuned;

diff -r f11bece4e2db -r aa757b35b129 NEWS
--- 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