NEWS
changeset 13280 306ef3aef61b
parent 13190 172f65d0c3d1
child 13284 20c818c966e6
     1.1 --- a/NEWS	Tue Jul 02 15:45:55 2002 +0200
     1.2 +++ b/NEWS	Tue Jul 02 15:54:21 2002 +0200
     1.3 @@ -1,6 +1,17 @@
     1.4 +
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 +New in this Isabelle release
     1.9 +----------------------------
    1.10 +
    1.11 +*** General ***
    1.12 +
    1.13 +* improved thms_containing: proper indexing of facts instead of raw
    1.14 +theorems; check validity of results wrt. current name space; include
    1.15 +local facts of proof configuration (also covers active locales);
    1.16 +
    1.17 +
    1.18  *** HOL ***
    1.19  
    1.20  * arith(_tac) does now know about div k and mod k where k is a numeral of
    1.21 @@ -10,6 +21,8 @@
    1.22  * simp's arithmetic capabilities have been enhanced a bit:
    1.23    it now takes ~= in premises into account (by performing a case split).
    1.24  
    1.25 +
    1.26 +
    1.27  New in Isabelle2002 (March 2002)
    1.28  --------------------------------
    1.29