# HG changeset patch
# User wenzelm
# Date 1014318692 -3600
# Node ID 02eb40cde931000cb05757bf7d2468a0a354c7a8
# Parent  9ba7c5358fa00c09edabe697175ec4705ca38564
* HOL: removed obsolete theorem "optionE";

diff -r 9ba7c5358fa0 -r 02eb40cde931 NEWS
--- 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);