* HOL: removed obsolete theorem "optionE";
authorwenzelm
Thu Feb 21 20:06:39 2002 +0100 (2002-02-21)
changeset 129170fd3caa5d8b2
parent 12916 4ac388e02b74
child 12918 bca45be2d25b
* HOL: removed obsolete theorem "optionE";
NEWS
     1.1 --- a/NEWS	Thu Feb 21 18:19:34 2002 +0100
     1.2 +++ b/NEWS	Thu Feb 21 20:06:39 2002 +0100
     1.3 @@ -226,7 +226,7 @@
     1.4  
     1.5  * HOL: linorder_less_split superseded by linorder_cases;
     1.6  
     1.7 -* HOL/List: "nodups" renamed to "distinct"
     1.8 +* HOL/List: "nodups" renamed to "distinct";
     1.9  
    1.10  * HOL: added "The" definite description operator; move Hilbert's "Eps"
    1.11  to peripheral theory "Hilbert_Choice";
    1.12 @@ -245,9 +245,9 @@
    1.13  a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be
    1.14  necessary to attach explicit type constraints;
    1.15  
    1.16 -* HOL/Relation: the prefix name of the infix "O" has been changed from "comp"
    1.17 -to "rel_comp"; INCOMPATIBILITY: a few theorems have been renamed accordingly
    1.18 -(eg "compI" -> "rel_compI").
    1.19 +* HOL/Relation: the prefix name of the infix "O" has been changed from
    1.20 +"comp" to "rel_comp"; INCOMPATIBILITY: a few theorems have been
    1.21 +renamed accordingly (eg "compI" -> "rel_compI").
    1.22  
    1.23  * HOL: syntax translations now work properly with numerals and records
    1.24  expressions;