minor updates to pre-2002 release
authorpaulson
Thu Feb 20 11:09:48 2003 +0100 (2003-02-20)
changeset 13824e4d8dea6dfc2
parent 13823 d49ffd9f9662
child 13825 ef4c41e7956a
minor updates to pre-2002 release
NEWS
     1.1 --- a/NEWS	Wed Feb 19 10:53:27 2003 +0100
     1.2 +++ b/NEWS	Thu Feb 20 11:09:48 2003 +0100
     1.3 @@ -401,6 +401,10 @@
     1.4  
     1.5  * HOL: canonical cases/induct rules for n-tuples (n = 3..7);
     1.6  
     1.7 +* HOL: consolidated and renamed several theories.  In particular:
     1.8 +	Ord.thy has been absorbed into HOL.thy
     1.9 +	String.thy has been absorbed into List.thy
    1.10 + 
    1.11  * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
    1.12  (beware of argument permutation!);
    1.13  
    1.14 @@ -409,7 +413,8 @@
    1.15  * HOL/List: "nodups" renamed to "distinct";
    1.16  
    1.17  * HOL: added "The" definite description operator; move Hilbert's "Eps"
    1.18 -to peripheral theory "Hilbert_Choice";
    1.19 +to peripheral theory "Hilbert_Choice"; some INCOMPATIBILITIES:
    1.20 +  - Ex_def has changed, now need to use some_eq_ex
    1.21  
    1.22  * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so
    1.23  in this (rare) case use: