* HOL: removed obsolete theorem "optionE";

--- a/NEWS	Thu Feb 21 20:11:05 2002 +0100
+++ b/NEWS	Thu Feb 21 20:11:32 2002 +0100
@@ -261,6 +261,9 @@
 
 * HOL: renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
 
+* HOL: removed obsolete theorem "optionE" (use "option.exhaust", or
+the "cases" method);
+
 * HOL/GroupTheory: group theory examples including Sylow's theorem (by
 Florian Kammüller);