# HG changeset patch
# User wenzelm
# Date 1014318399 -3600
# Node ID 0fd3caa5d8b2b4aa643f686435d64cc655d1b976
# Parent  4ac388e02b74bbae9e44e7f898593610872b35f9
* HOL: removed obsolete theorem "optionE";

diff -r 4ac388e02b74 -r 0fd3caa5d8b2 NEWS
--- a/NEWS	Thu Feb 21 18:19:34 2002 +0100
+++ b/NEWS	Thu Feb 21 20:06:39 2002 +0100
@@ -226,7 +226,7 @@
 
 * HOL: linorder_less_split superseded by linorder_cases;
 
-* HOL/List: "nodups" renamed to "distinct"
+* HOL/List: "nodups" renamed to "distinct";
 
 * HOL: added "The" definite description operator; move Hilbert's "Eps"
 to peripheral theory "Hilbert_Choice";
@@ -245,9 +245,9 @@
 a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be
 necessary to attach explicit type constraints;
 
-* HOL/Relation: the prefix name of the infix "O" has been changed from "comp"
-to "rel_comp"; INCOMPATIBILITY: a few theorems have been renamed accordingly
-(eg "compI" -> "rel_compI").
+* HOL/Relation: the prefix name of the infix "O" has been changed from
+"comp" to "rel_comp"; INCOMPATIBILITY: a few theorems have been
+renamed accordingly (eg "compI" -> "rel_compI").
 
 * HOL: syntax translations now work properly with numerals and records
 expressions;